[Merged by Bors] - feat(UniformSpace) : TotallyBounded + countably generated -> Separable

[JADekker]

Just a small result, that TotallyBounded sets are Separable sets in Uniform spaces with countably generated uniformities.

---

[urkud]

I've just noticed that EMetric.subset_countable_closure_of_almost_dense_set is a stronger version of the lemma you're proving: it assumes Countable instead of Finite, and provides a subset of s (in fact, it's used in Mathlib to prove that IsSeparable is equivalent to SeparableSpace in a metrizable topology).

[JADekker]

I've just noticed that EMetric.subset_countable_closure_of_almost_dense_set is a stronger version of the lemma you're proving: it assumes Countable instead of Finite, and provides a subset of s (in fact, it's used in Mathlib to prove that IsSeparable is equivalent to SeparableSpace in a metrizable topology).

You are right, @urkud. Are you suggesting that I close this PR, or would a refactor of my proof using this result still be valuable (as it would make sure that the necessary result turns up in moogle/loogle)? I just shortened the proof using this result, but I'm also happy to close the PR and only use this result in the original PR where I needed this (#12394).

[urkud]

Please reuse {X : Type*} from variables above. Also, please mention EMetric.subset_countable_closure_of_almost_dense_set in the docstring. Otherwise LGTM. Thanks!

bors d+

[mathlib-bors]

✌️ JADekker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[urkud]

We have these predicates as defs, so I think that having this version of the theorem definitely makes sense.

[JADekker]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style