proposition: Lemma segment_mono_surj_continuous a b f : monotonous `[a, b] f -> set_surj `[a, b] (f @`[a, b]) f -> {within `[a, b], continuous f}.
proof: Proof. rewrite continuous_subspace_in => -[fle|fge] f_surj x /set_mem /= xab. have leab : a <= b by rewrite (itvP xab). have fafb : f a <= f b by rewrite fle // ?bound_itvE. by apply: segment_inc_surj_continuous => //; case: ltrP f_surj fafb. have leab : a <= b by rewrite (itvP xab). have fafb : f b <= f a by rewrite fge // ?bound_itvE. by apply: segment_dec_surj_continuous => //; case: ltrP f_surj fafb. 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)