ofInjective_symm_apply — Mathlib

English

The inverse of the equivalence given by an injective f coincides with the range splitting map; equivalently, the inverse part of the injective equivalence equals rangeSplitting f as functions.

Русский

Обратная часть эквивалентности, заданной инъективной функцией, совпадает с отображением rangeSplitting f как функция.

LaTeX

$$$ (ofInjective\\ f\\ hf).symm = rangeSplitting f $ как отображения$$

Lean4

@[simp]
theorem ofInjective_symm_apply {α β} {f : α → β} (hf : Injective f) (a : α) :
    (ofInjective f hf).symm ⟨f a, ⟨a, rfl⟩⟩ = a :=
  by
  apply (ofInjective f hf).injective
  simp

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