subset_interior_succ

Mathlib.Topology.Compactness.SigmaCompact

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

English

In a compact exhaustion K of a space, each piece is contained in the interior of the next: K_n ⊆ int(K_{n+1}).

Русский

В компактной экспансии K каждой части принадлежит внутренности следующей: K_n ⊆ int(K_{n+1}).

LaTeX

$$$\forall n, K(n) \subseteq \operatorname{Int}(K(n+1))$$$

Lean4

theorem subset_interior_succ (n : ℕ) : K n ⊆ interior (K (n + 1)) :=
  K.subset_interior_succ' n

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

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

Разделы

Аффилиация

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