skeleton_top

Mathlib.Topology.CWComplex.Classical.Basic

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

English

The skeleton with top equals the base skeleton: skeleton(C; ⊤) = C.

Русский

Скелет с верхним уровнем равен всему комплексу: skeleton(C; ⊤) = C.

LaTeX

$$$\\mathrm{skeleton}(C;n)=\\mathrm{ skeletonLT}(C; n+1) \\ (n=\\top)$$$

Lean4

@[simp]
theorem skeleton_top [RelCWComplex C D] : skeleton C ⊤ = C :=
  skeletonLT_top

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

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

Разделы

Аффилиация

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