proposition: Lemma connected_continuous_connected (T U : topologicalType) (A : set T) (f : T -> U) : connected A -> {within A, continuous f} -> connected (f @` A).
proof: Proof. move=> cA cf; apply: contrapT => /connectedPn[E [E0 fAE sE]]. set AfE := fun b =>(A `&` f @^-1` E b) : set (subspace A). suff sAfE : separated (AfE false) (AfE true). move: cA; apply/connectedPn; exists AfE; split; last (rewrite /AfE; split). - move=> b; case: (E0 b) => /= u Ebu. have [t Et ftu] : (f @` A) u by rewrite fAE; case: b Ebu; [right|left]. by exists t; split => //=; rewrite /preimage ftu. - by rewrite -setIUr -preimage_setU -fAE; exact/esym/setIidPl/preimage_image. + rewrite -{2}(setIid A) ?setIA -(@closure_subspaceW _ A); last by move=> ?[]. by rewrite -/(AfE false) -setIA -/(AfE true); case: sAfE. + rewrite -{1}(setIid A) setIC ?setIA -(@closure_subspaceW _ A). by rewrite -/(AfE true) -setIA -/(AfE false) setIC; case: sAfE. by move=> ?[]. suff cI0 b : closure (AfE b) `&` AfE (~~ b) = set0. by rewrite /separated cI0 setIC cI0. have [fAfE cEIE] : f @` AfE (~~ b) = E (~~ b) /\ closure (E b) `&` E (~~ b) = set0. split; last by case: sE => ? ?; case: b => //; rewrite setIC. rewrite eqEsubset; split => [|u Ebu]. apply: (subset_trans sub_image_setI). by apply: subIset; right; exact: image_preimage_subset. have [t [At ftu]] : exists t, A t /\ f t = u. suff [t At ftu] : (f @` A) u by exists t. by rewrite fAE; case: b Ebu; [left|right]. by exists t => //; split => //=; rewrite /preimage ftu. have ? : f @` closure (AfE b) `<=` closure (E b). have /(@image_subset _ _ f) : closure (AfE b) `<=` f @^-1` closure (E b). have /closure_id -> : closed (f @^-1` closure (E b) : set (subspace A)). by apply: closed_comp => //; exact: closed_closure. apply: closure_subset. have /(@preimage_subset _ _ f) A0cA0 := @subset_closure _ (E b). by apply: subset_trans A0cA0; apply: subIset; right. by move/subset_trans; apply; exact: image_preimage_subset. apply/eqP/negPn/negP/set0P => -[t [? ?]]. have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0. by rewrite fAfE; exact: subsetI_eq0 cEIE. by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply: fcAfEb; split; exists t. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed