IccExtend_range — Mathlib

English

Let f be a function defined on the closed interval [a, b]. Extending f to the whole line with IccExtend preserves its range: the image of the extension equals the image of f.

Русский

Пусть f задана на замкнутом интервале [a, b]. Расширение f до всей прямой с помощью IccExtend сохраняет диапазон: образ расширения равен образу f.

LaTeX

$$$\\operatorname{range}(\\mathrm{IccExtend} h f) = \\operatorname{range} f$$$

Lean4

@[simp]
theorem IccExtend_range (f : Icc a b → β) : range (IccExtend h f) = range f := by
  simp only [IccExtend, range_comp f, range_projIcc, image_univ]

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