separableSpace — Mathlib

English

If s is separable, then the subspace s is separable.

Русский

Если s разделимо, то подпространство s тоже разделимо.

LaTeX

$$SeparableSpace s$$

Lean4

/-- If a set `s` is separable, then the corresponding subtype is separable in a (pseudo extended)
metric space.  This is not obvious, as the countable set whose closure covers `s` does not need in
general to be contained in `s`. -/
theorem separableSpace {s : Set α} (hs : IsSeparable s) : SeparableSpace s :=
  by
  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, hst⟩
  lift t to Set s using hts
  refine ⟨⟨t, countable_of_injective_of_countable_image Subtype.coe_injective.injOn htc, ?_⟩⟩
  rwa [IsInducing.subtypeVal.dense_iff, Subtype.forall]

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