mapsTo_Ioo — Mathlib

English

If f is strictly monotone on Icc a b, then f maps Ioo a b into Ioo f(a) f(b).

Русский

Если f строго монотонна на Icc a b, то образ Ioo a b лежит в Ioo f(a) f(b).

LaTeX

$$$$ \\forall x\\; (a < x < b)\\;:\\; f(a) < f(x) < f(b). $$$$

Lean4

theorem mapsTo_Ioo (h : StrictMonoOn f (Icc a b)) : MapsTo f (Ioo a b) (Ioo (f a) (f b)) := fun _c hc ↦
  ⟨h (left_mem_Icc.2 (hc.1.trans hc.2).le) (Ioo_subset_Icc_self hc) hc.1,
    h (Ioo_subset_Icc_self hc) (right_mem_Icc.2 (hc.1.trans hc.2).le) hc.2⟩

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