skeletonLT_top

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.RelCWComplex.skeletonLT_top

English

For any RelCWComplex, skeletonLT(C D; ⊤) = C; the LT-skeleton with the top level recovers the whole complex.

Русский

Для любого RelCWComplex скелет LT при верхнем уровне даёт весь комплекс.

LaTeX

$$$\\mathrm{skeletonLT}(C,D;\\top)=C$$$

Lean4

@[simp]
theorem skeletonLT_top [RelCWComplex C D] : skeletonLT C ⊤ = C := by simp [coe_skeletonLT, union]

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

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

Разделы

Аффилиация

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