sumCongr_refl

Mathlib.Topology.Constructions.SumProd

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

English

Sum of identity homeomorphisms is the identity homeomorphism on the sum.

Русский

Сумма тождественных гомеоморфизмов равна тождественному гомеоморфизму над суммой.

LaTeX

$$$$\\mathrm{sumCongr}((\\mathrm{refl}\,X), (\\mathrm{refl}\\,Y)) = \\mathrm{refl}(X ⊕ Y).$$$$

Lean4

@[simp]
theorem sumCongr_refl : sumCongr (.refl X) (.refl Y) = .refl (X ⊕ Y) :=
  by
  ext i
  cases i <;> rfl

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

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

Разделы

Аффилиация

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