subset_interior

Mathlib.Topology.Compactness.SigmaCompact

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

English

For every x in X, there exists an index n with x ∈ K_n.

Русский

Для каждого x ∈ X существует индекс n, такой что x ∈ K_n.

LaTeX

$$$$\forall x\in X, \exists n, x \in K_n.$$$$

Lean4

theorem subset_interior ⦃m n : ℕ⦄ (h : m < n) : K m ⊆ interior (K n) :=
  Subset.trans (K.subset_interior_succ m) <| interior_mono <| K.subset h

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

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

Разделы

Аффилиация

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