mapsTo_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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