equivCongr_refl — Mathlib

English

The equivCongr of identity on α and β is the identity on (α ≃ β): (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β).

Русский

Эквивалентность переносит тождественное отображение в тождество между α ≃ β: (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β).

LaTeX

$$$(\\mathrm{Equiv.refl }\\alpha).equivCongr (\\mathrm{Equiv.refl }\\beta) = \\mathrm{Equiv.refl }(\\alpha \\simeq \\beta)$$$

Lean4

@[simp]
theorem equivCongr_refl {α β} : (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β) := by grind

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