rangeSplitting — Mathlib

English

Let f: A → B. There exists a function g: range(f) → A such that for every y ∈ range(f), f(g(y)) = y.

Русский

Пусть f: A → B. Существуют такая отображение g: range(f) → A, что для каждого y ∈ range(f) выполняется f(g(y)) = y.

LaTeX

$$$$\\exists g: \\mathrm{range}(f) \\to \\alpha,\\; \\forall y \\,( y \\in \\mathrm{range}(f) \\rightarrow f(g(y)) = y ).$$$$

Lean4

/-- We can use the axiom of choice to pick a preimage for every element of `range f`. -/
noncomputable def rangeSplitting (f : α → β) : range f → α := fun x => x.2.choose

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