range_IciExtend — Mathlib

English

For any f: Ici a → β, the range (image) of the extension IciExtend f equals the range of f. In other words, extending f along the ray does not create new values.

Русский

Для любого f: Ici a → β область значений расширения IciExtend f совпадает с областью значений f.

LaTeX

$$$$\\operatorname{range}(\\IciExtend f) = \\operatorname{range}(f).$$$$

Lean4

@[simp]
theorem range_IciExtend (f : Ici a → β) : range (IciExtend f) = range f := by
  simp only [IciExtend, range_comp f, range_projIci, image_univ]

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