exists_countable_dense_subset — Mathlib

English

Let α be a topological space with a dense subspace s that is separable; then there exists a countable subset t of s that is dense in s (hence dense in α).

Русский

Пусть α имеет плотное подпространство s, которое сепарабельно; тогда существует счётное подмножество t ⊆ s, плотное в s (а значит и в α).

LaTeX

$$$\\exists t \\subseteq s, \\ t.Countable \\wedge Dense\ t$$$

Lean4

theorem exists_countable_dense_subset {α : Type*} [TopologicalSpace α] {s : Set α} [SeparableSpace s] (hs : Dense s) :
    ∃ t ⊆ s, t.Countable ∧ Dense t :=
  let ⟨t, htc, htd⟩ := exists_countable_dense s
  ⟨(↑) '' t, Subtype.coe_image_subset s t, htc.image Subtype.val,
    hs.denseRange_val.dense_image continuous_subtype_val htd⟩

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