mapsTo_Ioo — Mathlib

English

If f is strictly antitone on Icc a b, then f maps Ioo a b into Ioo b.rev a.rev.

Русский

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

LaTeX

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

Lean4

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

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