proposition: Lemma segment_inc_surj_continuous a b f : {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f -> {within `[a, b], continuous f}.
proof: Proof. move=> fle f_surj; have [f_inj flt] := (inc_inj_in fle, leW_mono_in fle). have [aLb|bLa|] := ltgtP a b; first last. - by move=> ->; rewrite set_itv1; exact: continuous_subspace1. - rewrite continuous_subspace_in => z /set_mem /=; rewrite in_itv /=. by move=> /andP[/le_trans] /[apply]; rewrite leNgt bLa. have le_ab : a <= b by rewrite ltW. have [aab bab] : a \in `[a, b] /\ b \in `[a, b] by rewrite !bound_itvE ltW. have fab : f @` `[a, b] = `[f a, f b]%classic by exact:inc_surj_image_segment. pose g := pinv `[a, b] f; have fK : {in `[a, b], cancel f g}. by rewrite -[mem _]mem_setE; apply: pinvKV; rewrite !mem_setE. have gK : {in `[f a, f b], cancel g f} by move=> z zab; rewrite pinvK// fab inE. have gle : {in `[f a, f b] &, {mono g : x y / x <= y}}. apply: can_mono_in (fle); first by move=> *; rewrite gK. move=> z zfab; have {zfab} : `[f a, f b]%classic z by []. by rewrite -fab => -[x xab <-]; rewrite fK. have glt := leW_mono_in gle. rewrite continuous_subspace_in => x xab. have xabcc : x \in `[a, b] by move: xab; rewrite mem_setE. have fxab : f x \in `[f a, f b] by rewrite in_itv/= !fle. have := xabcc; rewrite in_itv //= => /andP [ax xb]. apply/cvgrPdist_lt => _ /posnumP[e]; rewrite !near_simpl; near=> y. rewrite (@le_lt_trans _ _ (e%:num / 2%:R))//; last first. by rewrite ltr_pdivrMr// ltr_pMr// ltr1n. rewrite ler_distlC; near: y. pose u := minr (f x + e%:num / 2) (f b). pose l := maxr (f x - e%:num / 2) (f a). have ufab : u \in `[f a, f b]. rewrite !in_itv /= le_minl ?le_minr lexx ?fle // le_ab orbT ?andbT. by rewrite ler_wpDr // fle. have lfab : l \in `[f a, f b]. rewrite !in_itv/= le_maxl ?le_maxr lexx ?fle// le_ab orbT ?andbT. by rewrite lerBlDr ler_wpDr// fle // lexx. have guab : g u \in `[a, b]. rewrite !in_itv; apply/andP; split; have := ufab; rewrite in_itv => /andP. by case; rewrite /= -[f _ <= _]gle // ?fK // bound_itvE fle. by case => _; rewrite /= -[_ <= f _]gle // ?fK // bound_itvE fle. have glab : g l \in `[a, b]. rewrite !in_itv; apply/andP; split; have := lfab; rewrite in_itv /= => /andP. by case; rewrite -[f _ <= _]gle // ?fK // bound_itvE fle. by case => _; rewrite -[_ <= f _]gle // ?fK // bound_itvE fle. have faltu : f a < u. rewrite /u comparable_lt_minr ?real_comparable ?num_real// flt// aLb andbT. by rewrite (@le_lt_trans _ _ (f x)) ?fle// ltrDl. have lltfb : l < f b. rewrite /u comparable_lt_maxl ?real_comparable ?num_real// flt// aLb andbT. by rewrite (@lt_le_trans _ _ (f x)) ?fle// ltrBlDr ltrDl. case: pselect => // _; rewrite near_withinE; near_simpl. have Fnbhs : Filter (nbhs x) by apply: nbhs_filter. have := ax; rewrite le_eqVlt => /orP[/eqP|] {}ax. near=> y => /[dup] yab; rewrite /= in_itv => /andP[ay yb]; apply/andP; split. by rewrite (@le_trans _ _ (f a)) ?fle// lerBlDr ax ler_wpDr. apply: ltW; suff : f y < u by rewrite lt_minr => /andP[->]. rewrite -?[f y < _]glt// ?fK//; last by rewrite in_itv /= !fle. by near: y; near_simpl; apply: open_lt; rewrite /= -flt ?gK// -ax. have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb]. near=> y => /[dup] yab; rewrite /= in_itv /= => /andP[ay yb]. apply/andP; split; last by rewrite (@le_trans _ _ (f b)) ?fle// xb ler_wpDr. apply: ltW; suff : l < f y by rewrite lt_maxl => /andP[->]. rewrite -?[_ < f y]glt// ?fK//; last by rewrite in_itv /= !fle. by near: y; near_simpl; apply: open_gt; rewrite /= -flt// gK// xb. have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split. near=> y; suff: l <= f y <= u. by rewrite le_maxl le_minr -!andbA => /and4P[-> _ ->]. have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv. have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW. rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //. apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=. rewrite -[x]fK // !glt//= lt_minr lt_maxl ?andbT ltrBlDr ltr_pwDr //. by apply/and3P; split; rewrite // flt. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)