coe_prodCongr

Mathlib.Topology.Constructions.SumProd

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

English

The underlying function of h1.prodCongr h2 coincides with the product map Prod.map h1 h2.

Русский

Базовая функция (underlying function) h1.prodCongr h2 совпадает с отображением Prod.map h1 h2.

LaTeX

$$$\IsOpenMap f \Rightarrow \text{(неформальная запись)}$$$

Lean4

@[simp]
theorem coe_prodCongr (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂ :=
  rfl

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

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

Разделы

Аффилиация

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