proposition: Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set_system T) (P : set U -> Prop) : (forall X Y, X `<=` Y -> P Y -> P X) -> ProperFilter F -> (\forall y \near powerset_filter_from F, P (f @` y)) = (\forall y \near powerset_filter_from (f x @[x --> F]), P y).
proof: Proof. move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map. case=> G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). exact: powerset_filter_from_filter. have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). by rewrite /fmap /=; apply: filterS; first exact: preimage_image. near=> M; have FfM : fmap f F M by exact: (near (near_small_set _) M). apply: (@Pmono _ (f @` D)); first exact: (near (small_set_sub ffiD) M). exact: GP. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed