interior_compact_eq_empty — Mathlib

English

If a subset s of the rationals is compact (in the usual topology), then its interior, relative to the rationals, is empty.

Русский

Если подмножество s ⊆ ℚ компактно в обычной топологии, то его interior в ℚ пусто.

LaTeX

$$$\operatorname{Int}(s)=\emptyset$ для всех компактных $s\subseteq\mathbb{Q}$$$

Lean4

theorem interior_compact_eq_empty (hs : IsCompact s) : interior s = ∅ :=
  isDenseEmbedding_coe_real.isDenseInducing.interior_compact_eq_empty dense_irrational hs

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