English
A set is separable if and only if its closure is separable.
Русский
Множество сепарабельно тогда и только тогда, когда его замыкание сепарабельно.
LaTeX
$$$IsSeparable(closure\ s) \iff IsSeparable(s)$$$
Lean4
/-- A set `s` in a topological space is separable if it is contained in the closure of a countable
set `c`. Beware that this definition does not require that `c` is contained in `s` (to express the
latter, use `TopologicalSpace.SeparableSpace s` or
`TopologicalSpace.IsSeparable (univ : Set s))`. In metric spaces, the two definitions are
equivalent, see `TopologicalSpace.IsSeparable.separableSpace`. -/
def IsSeparable (s : Set α) :=
∃ c : Set α, c.Countable ∧ s ⊆ closure c
