isSeparable — Mathlib

English

Every compact subset of a pseudometric space is separable.

Русский

Каждый компактный подмножество псевдометрического пространства сепарабельно.

LaTeX

$$$\\forall s\\, (\\text{IsCompact } s) \\Rightarrow \\text{IsSeparable } s$$$

Lean4

/-- A compact set is separable. -/
theorem isSeparable {s : Set α} (hs : IsCompact s) : IsSeparable s :=
  haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
  .of_subtype s

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