strictMonoOn_of_injOn_Icc' — Mathlib

English

If f is continuous and injective on (a, b), then f is strictly monotone or strictly anti on (a, b).

Русский

Если f непрерывна и инъективна на (a, b), тогда f либо строго возрастает, либо строго убывает на (a, b).

LaTeX

$$StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)$$

Lean4

/-- Suppose `f : [a, b] → δ` is continuous and injective. Then `f` is strictly monotone
or antitone (increasing or decreasing). -/
theorem strictMonoOn_of_injOn_Icc' {a b : α} {f : α → δ} (hab : a ≤ b) (hf_c : ContinuousOn f (Icc a b))
    (hf_i : InjOn f (Icc a b)) : StrictMonoOn f (Icc a b) ∨ StrictAntiOn f (Icc a b) :=
  (le_total (f a) (f b)).imp (ContinuousOn.strictMonoOn_of_injOn_Icc hab · hf_c hf_i)
    (ContinuousOn.strictAntiOn_of_injOn_Icc hab · hf_c hf_i)

Похожие утверждения