range_IicExtend — Mathlib

English

Let f be a function defined on the downward interval (-∞, b]. Extending f to the whole line via IicExtend does not change its range; the image of the extension equals the image of f.

Русский

Пусть f задана на интервале (-∞, b]. Расширение f до всей окружности линейного порядка по операции IicExtend имеет тот же образ, что и f.

LaTeX

$$$\\operatorname{range}(\\mathrm{IicExtend} f) = \\operatorname{range} f$$$

Lean4

@[simp]
theorem range_IicExtend (f : Iic b → β) : range (IicExtend f) = range f := by
  simp only [IicExtend, range_comp f, range_projIic, image_univ]

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