proposition: Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set_system T) (P : set U -> Prop) : ProperFilter F -> (\forall y \near powerset_filter_from (f x @[x --> F]), P y) -> (\forall y \near powerset_filter_from F, P (f @` y)).
proof: Proof. move=> FF [] G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from F). exact: powerset_filter_from_filter. have /= := Gf _ GD; rewrite nbhs_simpl => FfD. near=> M; apply: GP; apply: (Gs D) => //. apply: filterS; first exact: preimage_image. exact: (near (near_small_set _) M). have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M). by move/image_subset/subset_trans; apply; exact: image_preimage_subset. 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