mapEquiv_refl — Mathlib

English

The mapEquiv construction sends identity equivalences to the identity equivalence on the mapped type.

Русский

Конструкция mapEquiv отображает тождественные эквивалентности в тождественные эквивалентности на отображаемом типе.

LaTeX

$$$\\text{mapEquiv } f (\\text{Equiv.refl } \\alpha) = \\text{Equiv.refl } (f \\alpha)$$$

Lean4

@[simp]
theorem mapEquiv_refl : mapEquiv f (Equiv.refl α) = Equiv.refl (f α) :=
  by
  ext x
  simp only [mapEquiv_apply, refl_apply]
  exact LawfulFunctor.id_map x

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