strictAntiOn_of_injOn_Icc — Mathlib

English

If a ≤ b and f(a) ≤ f(b) with continuity on [a, b], then StrictMonoOn f on Icc a b.

Русский

Если a ≤ b и f(a) ≤ f(b) при непрерывности на [a, b], то f строго монотонна на Icc a b.

LaTeX

$$StrictMonoOn f (Icc a b)$$

Lean4

/-- Suppose `f : [a, b] → δ` is
continuous and injective. Then `f` is strictly antitone (decreasing) if `f(b) ≤ f(a)`. -/
theorem strictAntiOn_of_injOn_Icc {a b : α} {f : α → δ} (hab : a ≤ b) (hfab : f b ≤ f a)
    (hf_c : ContinuousOn f (Icc a b)) (hf_i : InjOn f (Icc a b)) : StrictAntiOn f (Icc a b) :=
  ContinuousOn.strictMonoOn_of_injOn_Icc (δ := δᵒᵈ) hab hfab hf_c hf_i

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