compactCovering_subset

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#compactCovering_subset

English

If m ≤ n, then compactCovering X m is contained in compactCovering X n.

Русский

Если m ≤ n, то compactCovering X m ⊆ compactCovering X n.

LaTeX

$$$\\forall m\\, \\forall n\\, (m \\le n) \\Rightarrow compactCovering X m \\subseteq compactCovering X n$$$

Lean4

@[mono, gcongr]
theorem compactCovering_subset ⦃m n : ℕ⦄ (h : m ≤ n) : compactCovering X m ⊆ compactCovering X n :=
  monotone_accumulate h

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

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

Разделы

Аффилиация

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