openCell_subset_closedCell

Mathlib.Topology.CWComplex.Classical.Basic

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

← MathLib Explorer

English

Each open cell is contained in its corresponding closed cell.

Русский

Каждая открытая клетка содержится в соответствующей ей закрытой клетке.

LaTeX

$$$openCell\ n\ i \subseteq closedCell\ n\ i$$$

Lean4

theorem openCell_subset_closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : openCell n i ⊆ closedCell n i :=
  image_mono Metric.ball_subset_closedBall

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

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

Разделы

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

Аффилиация

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