mapsTo

Mathlib.Topology.CWComplex.Classical.Basic

URI: https://scilib.ai/kg/mathlib#Topology.CWComplex.mapsTo

← MathLib Explorer

English

For any cell i in C, openCell n i is disjoint from D.

Русский

Для любой клетки i в C, openCell n i дисjoint от D.

LaTeX

$$$Disjoint\ (openCell\ n\ i)\ D$$$

Lean4

theorem mapsTo [CWComplex C] (n : ℕ) (i : cell C n) :
    ∃ I : Π m, Finset (cell C m), MapsTo (map n i) (sphere 0 1) (⋃ (m < n) (j ∈ I m), map m j '' closedBall 0 1) :=
  by
  have := RelCWComplex.mapsTo n i
  simp_rw [empty_union] at this
  exact this

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

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

Разделы

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

Аффилиация

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