leftInverse_rangeSplitting — 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 leftInverse_rangeSplitting (f : α → β) : LeftInverse (rangeFactorization f) (rangeSplitting f) := fun x =>
  by
  ext
  simp only [rangeFactorization_coe]
  apply apply_rangeSplitting

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