coe_refl — Mathlib

English

The canonical identity equivalence acts as the identity function; the map refl α corresponds to id on α.

Русский

Единичная эквивалентность действуют как тождественная функция; отображение refl α соответствует идентичности на α.

LaTeX

$$$(\\mathrm{Equiv.refl}(\\alpha):\\alpha\\to\\alpha)=\\mathrm{id}_{\\alpha}.$$$

Lean4

@[simp]
theorem coe_refl : (Equiv.refl α : α → α) = id :=
  rfl

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