proposition: Lemma itv_continuous_inj_le f (I : interval R) : (exists x y, [/\ x \in I, y \in I, x < y & f x <= f y]) -> {within [set` I], continuous f} -> {in I &, injective f} -> {in I &, {mono f : x y / x <= y}}.
proof: Proof. gen have fxy : f / {in I &, injective f} -> {in I &, forall x y, x < y -> f x != f y}. move=> fI x y xI yI xLy; apply/negP => /eqP /fI => /(_ xI yI) xy. by move: xLy; rewrite xy ltxx. gen have main : f / forall c, {within [set` I], continuous f} -> {in I &, injective f} -> {in I &, forall a b, f a < f b -> a < c -> c < b -> f a < f c /\ f c < f b}. move=> c fC fI a b aI bI faLfb aLc cLb. have intP := interval_is_interval aI bI. have cI : c \in I by rewrite intP// (ltW aLc) ltW. have ctsACf : {within `[a, c], continuous f}. apply: (continuous_subspaceW _ fC) => x; rewrite /= inE => /itvP axc. by rewrite intP// axc/= (le_trans _ (ltW cLb))// axc. have ctsCBf : {within `[c, b], continuous f}. apply: (continuous_subspaceW _ fC) => x /=; rewrite inE => /itvP axc. by rewrite intP// axc andbT (le_trans (ltW aLc)) ?axc. have [aLb alb'] : a < b /\ a <= b by rewrite ltW (lt_trans aLc). have [faLfc|fcLfa|/eqP faEfc] /= := ltrgtP (f a) (f c). - split; rewrite // lt_neqAle fxy // leNgt; apply/negP => fbLfc. have := fbLfc; suff /eqP -> : c == b by rewrite ltxx. rewrite eq_le (ltW cLb) /=. have [d /andP[ad dc] fdEfb] : exists2 d, a <= d <= c & f d = f b. have aLc' : a <= c by rewrite ltW. apply: IVT => //; last first. by case: ltrgtP faLfc; rewrite // (ltW faLfb) // ltW. rewrite -(fI _ _ _ _ fdEfb) //. move: ad dc; rewrite le_eqVlt =>/predU1P[<-//| /ltW L] dc. by rewrite intP// L (le_trans _ (ltW cLb)). - have [fbLfc | fcLfb | fbEfc] /= := ltrgtP (f b) (f c). + by have := lt_trans fbLfc fcLfa; rewrite ltNge (ltW faLfb). + have [d /andP[cLd dLb] /eqP] : exists2 d, c <= d <= b & f d = f a. have cLb' : c <= b by rewrite ltW. apply: IVT => //; last by case: ltrgtP fcLfb; rewrite // !ltW. have /(fxy f fI) : a < d by rewrite (lt_le_trans aLc). suff dI' : d \in I by rewrite eq_sym=> /(_ aI dI') => /negbTE ->. move: dLb; rewrite le_eqVlt => /predU1P[->//|/ltW db]. by rewrite intP// db (le_trans (ltW aLc)). + by move: fcLfa; rewrite -fbEfc ltNge (ltW faLfb). by move/(fxy _ fI) : aLc=> /(_ aI cI); rewrite faEfc. move=> [u [v [uI vI ulv +]]] fC fI; rewrite le_eqVlt => /predU1P[fufv|fuLfv]. by move/fI: fufv => /(_ uI vI) uv; move: ulv; rewrite uv ltxx. have aux a c b : a \in I -> b \in I -> a < c -> c < b -> (f a < f c -> f a < f b /\ f c < f b) /\ (f c < f b -> f a < f b /\ f a < f c). move=> aI bI aLc cLb; have aLb := lt_trans aLc cLb. have cI : c \in I by rewrite (interval_is_interval aI bI)// (ltW aLc)/= ltW. have fanfb : f a != f b by apply: (fxy f fI). have decr : f b < f a -> f b < f c /\ f c < f a. have ofC : {within [set` I], continuous (-f)}. move=> ?; apply: continuous_comp; [exact: fC | exact: continuousN]. have ofI : {in I &, injective (-f)} by move=>> ? ? /oppr_inj/fI ->. rewrite -[X in X < _ -> _](opprK (f b)) ltrNl => ofaLofb. have := main _ c ofC ofI a b aI bI ofaLofb aLc cLb. by (do 2 rewrite ltrNl opprK); rewrite and_comm. split=> [faLfc|fcLfb]. suff L : f a < f b by have [] := main f c fC fI a b aI bI L aLc cLb. by case: ltgtP decr fanfb => // fbfa []//; case: ltgtP faLfc. suff L : f a < f b by have [] := main f c fC fI a b aI bI L aLc cLb. by case: ltgtP decr fanfb => // fbfa []//; case: ltgtP fcLfb. have{main fC} whole a c b := main f c fC fI a b. have low a c b : f a < f c -> a \in I -> b \in I -> a < c -> c < b -> f a < f b /\ f c < f b. by move=> L aI bI ac cb; case: (aux a c b aI bI ac cb)=> [/(_ L)]. have high a c b : f c < f b -> a \in I -> b \in I -> a < c -> c < b -> f a < f b /\ f a < f c. by move=> L aI bI ac cb; case: (aux a c b aI bI ac cb)=> [_ /(_ L)]. apply: le_mono_in => x y xI yI xLy. have [uLx | xLu | xu] := ltrgtP u x. - suff fuLfx : f u < f x by have [] := low u x y fuLfx uI yI uLx xLy. have [xLv | vLx | -> //] := ltrgtP x v; first by case: (whole u x v). by case: (low u v x). - have fxLfu : f x < f u by have [] := high x u v fuLfv xI vI xLu ulv. have [yLu | uLy | -> //] := ltrgtP y u; first by case: (whole x y u). by case: (low x u y). move: xLy; rewrite -xu => uLy. have [yLv | vLy | -> //] := ltrgtP y v; first by case: (whole u y v). by case: (low u v y). 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)