skeletonLT_zero_eq_base

Mathlib.Topology.CWComplex.Classical.Basic

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

English

If C D form a RelCWComplex, then the 0-th skeleton LT is exactly the base D.

Русский

Пусть C D образуют RelCWComplex; нулевой LT-скелет равен базовой множеству D.

LaTeX

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

Lean4

theorem skeletonLT_zero_eq_base [RelCWComplex C D] : skeletonLT C 0 = D := by simp [coe_skeletonLT]

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

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

Разделы

Аффилиация

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