self_comp_ofInjective_symm — Mathlib

English

If f is injective, then f ∘ (ofInjective f hf).symm = Subtype.val.

Русский

Если f инъективна, то композиция f с обратным отображением (ofInjective f hf).symm равна Subtype.val.

LaTeX

$$$f \\circ (\\mathrm{ofInjective} f hf).symm = \\mathrm{Subtype.val}$$$

Lean4

@[simp]
theorem self_comp_ofInjective_symm {α β} {f : α → β} (hf : Injective f) : f ∘ (ofInjective f hf).symm = Subtype.val :=
  funext fun x => apply_ofInjective_symm hf x

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