English
If a < b and f is continuous on (a, b) and injective, then f is strictly monotone or strictly anti on (a, b).
Русский
Если a < b, и f непрерывна на (a, b) и инъективна, тогда f строго монотонна или строго антимонотонна на (a, b).
LaTeX
$$StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)$$
Lean4
/-- Suppose `α` is equipped with a conditionally complete linear dense order and `f : α → δ` is
continuous and injective. Then `f` is strictly monotone or antitone (increasing or decreasing). -/
theorem strictMono_of_inj {f : α → δ} (hf_c : Continuous f) (hf_i : Injective f) : StrictMono f ∨ StrictAnti f :=
by
have H {c d : α} (hcd : c < d) : StrictMono f ∨ StrictAnti f :=
(hf_c.continuousOn.strictMonoOn_of_injOn_Icc' hcd.le hf_i.injOn).imp (hf_c.strictMonoOn_of_inj_rigidity hf_i hcd)
(hf_c.strictMonoOn_of_inj_rigidity (δ := δᵒᵈ) hf_i hcd)
cases subsingleton_or_nontrivial α with
| inl h => exact Or.inl <| Subsingleton.strictMono f
| inr h =>
obtain ⟨a, b, hab⟩ := exists_pair_lt α
exact H hab
