closedCell

Mathlib.Topology.CWComplex.Classical.Basic

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

← MathLib Explorer

English

The closed n-cell is the image of closedBall under the map of i.

Русский

Закрытая n-клетка — образ closedBall под отображением i.

LaTeX

$$$closedCell\; (n)\; (i) = map\; n\; i '' closedBall\ 0\ 1$$$

Lean4

/-- The closed `n`-cell given by the index `i`. Use this instead of `map n i '' closedBall 0 1`
whenever possible. -/
def closedCell [RelCWComplex C D] (n : ℕ) (i : cell C n) : Set X :=
  map n i '' closedBall 0 1

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

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

Разделы

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

Аффилиация

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