mapsTo_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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