English
If f is continuous on [a, b], injective on [a, b], and f(a) ≤ f(b), then f is strictly increasing on [a, b].
Русский
Если f непрерывна на [a,b], инъективна на [a,b], и f(a) ≤ f(b), то f строго возрастает на [a,b].
LaTeX
$$StrictMonoOn f (Icc a b)$$
Lean4
/-- Suppose `α` is equipped with a conditionally complete linear dense order and `f : α → δ` is
continuous and injective. Then `f` is strictly monotone (increasing) if
it is strictly monotone (increasing) on some closed interval `[a, b]`. -/
theorem strictMonoOn_of_inj_rigidity {f : α → δ} (hf_c : Continuous f) (hf_i : Injective f) {a b : α} (hab : a < b)
(hf_mono : StrictMonoOn f (Icc a b)) : StrictMono f :=
by
intro x y hxy
let s := min a x
let t := max b y
have hsa : s ≤ a := min_le_left a x
have hbt : b ≤ t := le_max_left b y
have hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t) :=
by
have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
have :=
Continuous.strictMono_of_inj_boundedOrder' (f := Set.restrict (Icc s t) f) hf_c.continuousOn.restrict
hf_i.injOn.injective
exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr
have (h : StrictAntiOn f (Icc s t)) : False :=
by
have : Icc a b ⊆ Icc s t := Icc_subset_Icc hsa hbt
replace : StrictAntiOn f (Icc a b) := StrictAntiOn.mono h this
replace : IsAntichain (· ≤ ·) (Icc a b) := IsAntichain.of_strictMonoOn_antitoneOn hf_mono this.antitoneOn
exact this.not_lt (left_mem_Icc.mpr (le_of_lt hab)) (right_mem_Icc.mpr (le_of_lt hab)) hab
replace hf_mono_st : StrictMonoOn f (Icc s t) := hf_mono_st.resolve_right this
have hsx : s ≤ x := min_le_right a x
have hyt : y ≤ t := le_max_right b y
replace : Icc x y ⊆ Icc s t := Icc_subset_Icc hsx hyt
replace : StrictMonoOn f (Icc x y) := StrictMonoOn.mono hf_mono_st this
exact this (left_mem_Icc.mpr (le_of_lt hxy)) (right_mem_Icc.mpr (le_of_lt hxy)) hxy
