apply

Mathlib.Topology.Homotopy.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousMap.HomotopyEquiv.Simps.apply

← MathLib Explorer

English

If X ≃ₕ Y and Z ≃ₕ Z', then X × Z ≃ₕ Y × Z'.

Русский

Если X ≃ₕ Y и Z ≃ₕ Z', тогда X × Z ≃ₕ Y × Z'.

LaTeX

$$$\text{prodCongr}(h_1:h_1: X\simeq_h Y, h_2: Z\simeq_h Z'):\; (X\times Z)\simeq_h (Y\times Z').$$$

Lean4

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections. -/
def apply (h : X ≃ₕ Y) : X → Y :=
  h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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