Theorem TopologicalSpace.IsSeparable.span

Modification history

2023-09-14 09:08
Mathlib/Topology/Algebra/Module/Basic.lean
feat: the linear span of a separable set is separable (#7115)
Added TopologicalSpace.IsSeparable.spanView on Github →