mapEquiv_refl_refl — Mathlib

English

The mapEquiv with identity equivalences on both sides yields the identity on F α α'.

Русский

MapEquiv с тождественными эквивалентностями на обе стороны даёт тождественный эквивалент на F α α'.

LaTeX

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

Lean4

@[simp]
theorem mapEquiv_refl_refl : mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α') :=
  by
  ext x
  simp [id_bimap]

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