proposition: Lemma ultra_image (T U : Type) (f : T -> U) (F : set_system T) : UltraFilter F -> f @` setT = setT -> UltraFilter [set f @` A | A in F].
proof: Proof. move=> FU fsurj; split; first exact: proper_image. move=> G GF sfFG; rewrite predeqE => A; split; last exact: sfFG. move=> GA; exists (f @^-1` A); last by rewrite image_preimage. have [//|FnAf] := in_ultra_setVsetC (f @^-1` A) FU. have : G (f @` (~` (f @^-1` A))) by apply: sfFG; exists (~` (f @^-1` A)). suff : ~ G (f @` (~` (f @^-1` A))) by []. rewrite preimage_setC image_preimage // => GnA. by have /filter_ex [? []] : G (A `&` (~` A)) by apply: filterI. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed