closedCell_subset_skeleton

Mathlib.Topology.CWComplex.Classical.Basic

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

English

In RelCWComplex C D, closedCell n j is contained in skeleton C n.

Русский

В RelCWComplex C D замкнутая клетка subset skeleton C n.

LaTeX

$$$\\text{closedCell}(n,j)\\subseteq \\mathrm{skeleton}(C,D;n)$$$

Lean4

theorem closedCell_subset_skeleton [RelCWComplex C D] (n : ℕ) (j : cell C n) : closedCell n j ⊆ skeleton C n :=
  closedCell_subset_skeletonLT n j

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

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

Разделы

Аффилиация

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