equivCongr_symm

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.equivCongr_symm

English

The symmetry commutes with equivCongr: (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm.

Русский

Симметрия коммутирует с equivCongr: (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm.

LaTeX

$$(ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm$$

Lean4

@[simp, grind =]
theorem equivCongr_symm {δ} (ab : α ≃ β) (cd : γ ≃ δ) : (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm := by ext;
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru