refl_toPartialEquiv — Mathlib

English

The identity equivalence on α, when viewed as a PartialEquiv, coincides with the identity PartialEquiv on α.

Русский

Тождественная эквивалентность на α, рассматриваемая как PartialEquiv, совпадает с тождественной PartialEquiv на α.

LaTeX

$$$(\\mathrm{Equiv.refl}\\,\\alpha).\\mathrm{toPartialEquiv} = \\mathrm{PartialEquiv.refl}\\alpha$$$

Lean4

@[simp, mfld_simps]
theorem refl_toPartialEquiv : (Equiv.refl α).toPartialEquiv = PartialEquiv.refl α :=
  rfl

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