rangeFactorization — Mathlib

English

Every map f: ι → α factors through its range via the map rangeFactorization f : ι → range f defined by i ↦ ⟨f i, mem_range_self i⟩.

Русский

Любое отображение f: ι → α факторизуется через образ range f: ι → range f, заданное i ↦ ⟨f i, mem_range_self i⟩.

LaTeX

$$$\\mathrm{rangeFactorization}(f) : ι \\to \\mathrm{range}(f),\\quad (i) \\mapsto \\langle f(i), \\mathrm{mem\\_range\_self}(i) \\rangle$$$

Lean4

/-- Any map `f : ι → α` factors through a map `rangeFactorization f : ι → range f`. -/
def rangeFactorization (f : ι → α) : ι → range f := fun i => ⟨f i, mem_range_self i⟩

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