uliftMap

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

URI: https://scilib.ai/kg/mathlib#ContinuousMap.Homotopy.uliftMap

Lean4

/-- Interpret a homotopy `H : C(I × X, Y)` as a map `C(ULift I × X, Y)` -/
def uliftMap : C(TopCat.of (ULift.{u} I × X), Y) :=
  ⟨fun x => H (x.1.down, x.2), H.continuous.comp ((continuous_uliftDown.comp continuous_fst).prodMk continuous_snd)⟩

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

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

Разделы

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

Аффилиация

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