subset

Mathlib.Topology.Compactness.SigmaCompact

URI: https://scilib.ai/kg/mathlib#CompactExhaustion.subset

English

If m ≤ n, then K_m ⊆ K_n; the sequence is increasing with the index.

Русский

Если m ≤ n, то K_m ⊆ K_n; последовательность возрастает по индексу.

LaTeX

$$$$m \le n \Rightarrow K_m \subseteq K_n.$$$$

Lean4

@[mono]
protected theorem subset ⦃m n : ℕ⦄ (h : m ≤ n) : K m ⊆ K n :=
  OrderHomClass.mono K h

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

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

Разделы

Аффилиация

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