mapsTo_Ioc — Mathlib

English

For f strictly antitone on [a,b], f maps the open interval (a,b) into (f(b), f(a)).

Русский

Для f строго антимонотонной на [a,b], отображение (a,b) в (f(b), f(a)).

LaTeX

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

Lean4

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

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