skeletonLT_monotone

Mathlib.Topology.CWComplex.Classical.Basic

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

English

The family skeletonLT(C,D;·) is monotone in its ENat index.

Русский

Семейство skeletonLT(C,D;·) монотонно по индексу ENat.

LaTeX

$$Monotone (skeletonLT C)$$

Lean4

theorem skeletonLT_monotone [RelCWComplex C D] : Monotone (skeletonLT C) := fun _ _ h ↦ skeletonLT_mono h

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

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

Разделы

Аффилиация

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