openCell_subset_skeletonLT

Mathlib.Topology.CWComplex.Classical.Basic

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

← MathLib Explorer

English

For RelCWComplex C D, and j ∈ cell C n, openCell n j is contained in skeletonLT C (n+1).

Русский

Для RelCWComplex C D и j∈cell C n, openCell n j ⊆ skeletonLT C (n+1).

LaTeX

$$$\\text{openCell}(n,j)\\subseteq \\mathrm{skeletonLT}(C,D;n+1)$$$

Lean4

theorem openCell_subset_skeletonLT [RelCWComplex C D] (n : ℕ) (j : cell C n) : openCell n j ⊆ skeletonLT C (n + 1) :=
  (openCell_subset_closedCell _ _).trans (closedCell_subset_skeletonLT _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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