Commit 2023-09-14 09:08 f16dbd9b

View on Github →

feat: the linear span of a separable set is separable (#7115)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff.lean

added theorem ContDiff.lipschitzWith_of_hasCompactSupport

Modified Mathlib/LinearAlgebra/Finsupp.lean

added theorem mem_span_set'

added theorem span_eq_iUnion_nat

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added theorem Submodule.closure_subset_topologicalClosure_span

added theorem TopologicalSpace.IsSeparable.span

Modified Mathlib/Topology/Bases.lean

added theorem TopologicalSpace.IsSeparable.prod

added theorem TopologicalSpace.isSeparable_pi

Modified Mathlib/Topology/EMetricSpace/Basic.lean

added theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset

Modified Mathlib/Topology/Separation.lean

added theorem nhdsWithin_compl_singleton_le