skeletonLT_zero_eq_empty

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.CWComplex.skeletonLT_zero_eq_empty

English

For a CW-complex C, skeletonLT(C, D; 0) is the empty set.

Русский

Для CW-комплекса C скелет LT при n = 0 пуст.

LaTeX

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

Lean4

theorem skeletonLT_zero_eq_empty [CWComplex C] : (skeletonLT C 0 : Set X) = ∅ :=
  RelCWComplex.skeletonLT_zero_eq_base

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

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

Разделы

Аффилиация

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