dense_compl_compact

Mathlib.Topology.Instances.RatLemmas

URI: https://scilib.ai/kg/mathlib#Rat.dense_compl_compact

English

For any compact s ⊆ ℚ, the complement sᶜ is dense in ℚ.

Русский

Для любого компактного множества s ⊆ ℚ дополнение s к ℚ плотно (модульоподобно) в ℚ.

LaTeX

$$$\text{Dense}(s^c)$$$

Lean4

theorem dense_compl_compact (hs : IsCompact s) : Dense sᶜ :=
  interior_eq_empty_iff_dense_compl.1 (interior_compact_eq_empty hs)

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

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

Разделы

Аффилиация

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