rangeFactorization_surjective — Mathlib

English

The map rangeFactorization f: ι → range f is surjective: for every y in range f there exists i with rangeFactorization f i = y.

Русский

Отображение rangeFactorization f: ι → range f сюръективно: для каждого y ∈ range f существует i такое, что rangeFactorization f i = y.

LaTeX

$$$$ \\forall y \\in \\operatorname{range}(f), \\exists i, \\operatorname{rangeFactorization} f i = y $$$$

Lean4

theorem rangeFactorization_surjective : Surjective (rangeFactorization f) := fun ⟨_, ⟨i, rfl⟩⟩ => ⟨i, rfl⟩

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