mapsTo_Ico — Mathlib

English

If f is strictly antitone, then f maps the open-closed interval (a,b] into (f(b), f(a)].

Русский

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

LaTeX

$$$f(Ioc(a,b)) \subseteq Ioc(f(b), f(a))$$$

Lean4

theorem mapsTo_Ico (h : StrictAntiOn f (Icc a b)) : MapsTo f (Ico a b) (Ioc (f b) (f a)) := fun _c hc ↦
  ⟨h (Ico_subset_Icc_self hc) (right_mem_Icc.2 <| hc.1.trans hc.2.le) hc.2,
    h.antitoneOn (left_mem_Icc.2 <| hc.1.trans hc.2.le) (Ico_subset_Icc_self hc) hc.1⟩

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