equivCongr_refl_right — Mathlib

English

Let α and β be types and ab: α ≃ β, e: α ≃ β. Then the left-conjugation of e by ab with the identity on β equals the composition ab.symm.trans e; i.e., ab.equivCongr (Equiv.refl β) e = ab.symm.trans e.

Русский

Пусть α и β — множества, и ab: α ≃ β, e: α ≃ β. Тогда левая конгруация e по ab с тождественным отображением на β равна композиции ab.symm.trans e; то есть ab.equivCongr (Equiv.refl β) e = ab.symm.trans e.

LaTeX

$$$ab\,.equivCongr(\mathrm{refl}\,\beta)\,e = ab^{-1}.trans e$$$

Lean4

@[simp]
theorem equivCongr_refl_right {α β} (ab e : α ≃ β) : ab.equivCongr (Equiv.refl β) e = ab.symm.trans e :=
  rfl

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