sumCongr_symm

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Homeomorph.sumCongr_symm

English

The sumCongr construction is symmetric with respect to taking inverses.

Русский

Конструкция sumCongr сохраняет симметрию при обращении.

LaTeX

$$$$ (\\mathrm{sumCongr}\\ h_1\\ h_2)^{-1} = \\mathrm{sumCongr}\\ h_1^{-1}\\ h_2^{-1}.$$$$

Lean4

@[simp]
theorem sumCongr_symm (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : (sumCongr h₁ h₂).symm = sumCongr h₁.symm h₂.symm :=
  rfl

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

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

Разделы

Аффилиация

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