skeleton_mono

Mathlib.Topology.CWComplex.Classical.Basic

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

English

The skeleton function is monotone: increasing n does not shrink the skeleton.

Русский

Функция скелета монотонна: при возрастании n скелет не уменьшается.

LaTeX

$$$n\\le m\\Rightarrow skeleton(C; n)\\subseteq skeleton(C; m)$$$

Lean4

theorem skeleton_mono [RelCWComplex C D] {n m : ℕ∞} (h : m ≤ n) : (skeleton C m : Set X) ⊆ skeleton C n :=
  skeletonLT_mono (add_le_add_right h 1)

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

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

Разделы

Аффилиация

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