English
If a ≤ b and f(a) ≤ f(b) and f is continuous on [a,b] with InjOn on [a,b], then f is strictly monotone on [a,b].
Русский
Если a ≤ b и f(a) ≤ f(b), и f непрерывна на [a,b] с InjOn на [a,b], тогда f строго монотонна на [a,b].
LaTeX
$$StrictMonoOn f (Icc a b)$$
Lean4
/-- Suppose `f : [a, b] → δ` is
continuous and injective. Then `f` is strictly monotone (increasing) if `f(a) ≤ f(b)`. -/
theorem strictMonoOn_of_injOn_Icc {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f a ≤ f b)
(hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) : StrictMonoOn f (Icc a b) :=
by
have : Fact (a ≤ b) := ⟨hab⟩
refine StrictMono.of_restrict ?_
set g : Icc a b → δ := Set.restrict (Icc a b) f
have hgab : g ⊥ ≤ g ⊤ := by aesop
exact Continuous.strictMono_of_inj_boundedOrder (f := g) hf_c.restrict hgab hf_i.injective
