coe_ofInjective_symm — Mathlib

English

Equality of the function obtained as the inverse of the injective equivalence with the rangeSplitting map holds on the nose.

Русский

Равенство функций, полученных как обратная часть эквивалентности инъективной функции и отображения rangeSplitting, истинно на уровне функций.

LaTeX

$$$ ((ofInjective f hf).symm : range f \\to α) = rangeSplitting f $$$

Lean4

theorem coe_ofInjective_symm {α β} {f : α → β} (hf : Injective f) :
    ((ofInjective f hf).symm : range f → α) = rangeSplitting f :=
  by
  ext ⟨y, x, rfl⟩
  apply hf
  simp [apply_rangeSplitting f]

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