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]