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

Mathlib/Analysis/Calculus/ContDiff.lean

@@ -2064,6 +2064,15 @@ theorem ContDiffAt.exists_lipschitzOnWith {f : E' → F'} {x : E'} (hf : ContDif
   (hf.hasStrictFDerivAt le_rfl).exists_lipschitzOnWith
 #align cont_diff_at.exists_lipschitz_on_with ContDiffAt.exists_lipschitzOnWith
 
+/-- A `C^1` function with compact support is Lipschitz. -/
+theorem ContDiff.lipschitzWith_of_hasCompactSupport {f : E' → F'} {n : ℕ∞}
+    (hf : HasCompactSupport f) (h'f : ContDiff 𝕂 n f) (hn : 1 ≤ n) :
+    ∃ C, LipschitzWith C f := by
+  obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)
+  refine ⟨⟨max C 0, le_max_right _ _⟩, ?_⟩
+  apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)
+  simp [← NNReal.coe_le_coe, hC x]
+
 end Real
 
 section deriv

Mathlib/LinearAlgebra/Finsupp.lean

@@ -1200,6 +1200,34 @@ theorem mem_span_set {m : M} {s : Set M} :
   exact Finsupp.mem_span_image_iff_total R (v := _root_.id (α := M))
 #align mem_span_set mem_span_set
 
+/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
+`m` can be written as a finite `R`-linear combination of elements of `s`.
+The implementation uses a sum indexed by `Fin n` for some `n`. -/
+lemma mem_span_set' {m : M} {s : Set M} :
+    m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → s),
+      ∑ i, f i • (g i : M) = m := by
+  refine ⟨fun h ↦ ?_, ?_⟩
+  · rcases mem_span_set.1 h with ⟨c, cs, rfl⟩
+    have A : c.support ≃ Fin c.support.card := Finset.equivFin _
+    refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩
+    rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]
+    exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)
+  · rintro ⟨n, f, g, rfl⟩
+    exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))
+
+/-- The span of a subset `s` is the union over all `n` of the set of linear combinations of at most
+`n` terms belonging to `s`. -/
+lemma span_eq_iUnion_nat (s : Set M) :
+    (Submodule.span R s : Set M) = ⋃ (n : ℕ),
+      (fun (f : Fin n → (R × M)) ↦ ∑ i, (f i).1 • (f i).2) '' ({f | ∀ i, (f i).2 ∈ s}) := by
+  ext m
+  simp only [SetLike.mem_coe, mem_iUnion, mem_image, mem_setOf_eq, mem_span_set']
+  refine exists_congr (fun n ↦ ⟨?_, ?_⟩)
+  · rintro ⟨f, g, rfl⟩
+    exact ⟨fun i ↦ (f i, g i), fun i ↦ (g i).2, rfl⟩
+  · rintro ⟨f, hf, rfl⟩
+    exact ⟨fun i ↦ (f i).1, fun i ↦ ⟨(f i).2, (hf i)⟩, rfl⟩
+
 /-- If `Subsingleton R`, then `M ≃ₗ[R] ι →₀ R` for any type `ι`. -/
 @[simps]
 def Module.subsingletonEquiv (R M ι : Type*) [Semiring R] [Subsingleton R] [AddCommMonoid M]

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -12,6 +12,7 @@ import Mathlib.Topology.UniformSpace.UniformEmbedding
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.Pi
+import Mathlib.LinearAlgebra.Finsupp
 
 #align_import topology.algebra.module.basic from "leanprover-community/mathlib"@"6285167a053ad0990fc88e56c48ccd9fae6550eb"
 
@@ -110,6 +111,21 @@ theorem continuousSMul_induced : @ContinuousSMul R M₁ _ u (t.induced f) := by
 
 end LatticeOps
 
+/-- The span of a separable subset with respect to a separable scalar ring is again separable. -/
+lemma TopologicalSpace.IsSeparable.span {R M : Type*} [AddCommMonoid M] [Semiring R] [Module R M]
+    [TopologicalSpace M] [TopologicalSpace R] [SeparableSpace R]
+    [ContinuousAdd M] [ContinuousSMul R M] {s : Set M} (hs : IsSeparable s) :
+    IsSeparable (Submodule.span R s : Set M) := by
+  rw [span_eq_iUnion_nat]
+  apply isSeparable_iUnion (fun n ↦ ?_)
+  apply IsSeparable.image
+  · have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
+      apply isSeparable_pi (fun i ↦ (isSeparable_of_separableSpace Set.univ).prod hs)
+    convert this
+    simp
+  · apply continuous_finset_sum _ (fun i _ ↦ ?_)
+    exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))
+
 namespace Submodule
 
 variable {α β : Type*} [TopologicalSpace β]
@@ -161,6 +177,11 @@ theorem Submodule.le_topologicalClosure (s : Submodule R M) : s ≤ s.topologica
   subset_closure
 #align submodule.le_topological_closure Submodule.le_topologicalClosure
 
+theorem Submodule.closure_subset_topologicalClosure_span (s : Set M) :
+    closure s ⊆ (span R s).topologicalClosure := by
+  rw [Submodule.topologicalClosure_coe]
+  exact closure_mono subset_span
+
 theorem Submodule.isClosed_topologicalClosure (s : Submodule R M) :
     IsClosed (s.topologicalClosure : Set M) := isClosed_closure
 #align submodule.is_closed_topological_closure Submodule.isClosed_topologicalClosure

Mathlib/Topology/Bases.lean

@@ -425,7 +425,7 @@ theorem _root_.Set.PairwiseDisjoint.countable_of_nonempty_interior [SeparableSpa
 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`. -/
+equivalent, see `TopologicalSpace.IsSeparable.separableSpace`. -/
 def IsSeparable (s : Set α) :=
   ∃ c : Set α, c.Countable ∧ s ⊆ closure c
 #align topological_space.is_separable TopologicalSpace.IsSeparable
@@ -457,6 +457,25 @@ theorem isSeparable_iUnion {ι : Type*} [Countable ι] {s : ι → Set α}
   exact (h'c i).trans (closure_mono (subset_iUnion _ i))
 #align topological_space.is_separable_Union TopologicalSpace.isSeparable_iUnion
 
+lemma isSeparable_pi {ι : Type*} [Fintype ι] {α : ∀ (_ : ι), Type*} {s : ∀ i, Set (α i)}
+    [∀ i, TopologicalSpace (α i)] (h : ∀ i, IsSeparable (s i)) :
+    IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i} := by
+  choose c c_count hc using h
+  refine ⟨{f | ∀ i, f i ∈ c i}, countable_pi c_count, ?_⟩
+  simp_rw [← mem_univ_pi]
+  dsimp
+  rw [closure_pi_set]
+  exact Set.pi_mono (fun i _ ↦ hc i)
+
+lemma IsSeparable.prod {β : Type*} [TopologicalSpace β]
+    {s : Set α} {t : Set β} (hs : IsSeparable s) (ht : IsSeparable t) :
+    IsSeparable (s ×ˢ t) := by
+  rcases hs with ⟨cs, cs_count, hcs⟩
+  rcases ht with ⟨ct, ct_count, hct⟩
+  refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩
+  rw [closure_prod_eq]
+  exact Set.prod_mono hcs hct
+
 theorem _root_.Set.Countable.isSeparable {s : Set α} (hs : s.Countable) : IsSeparable s :=
   ⟨s, hs, subset_closure⟩
 #align set.countable.is_separable Set.Countable.isSeparable

Mathlib/Topology/EMetricSpace/Basic.lean

@@ -809,17 +809,25 @@ theorem subset_countable_closure_of_almost_dense_set (s : Set α)
 #align emetric.subset_countable_closure_of_almost_dense_set EMetric.subset_countable_closure_of_almost_dense_set
 
 open TopologicalSpace in
-/-- 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 _root_.TopologicalSpace.IsSeparable.separableSpace {s : Set α} (hs : IsSeparable s) :
-    SeparableSpace s := by
+/-- If a set `s` is separable in a (pseudo extended) metric space, then it admits a countable dense
+subset. This is not obvious, as the countable set whose closure covers `s` given by the definition
+of separability does not need in general to be contained in `s`. -/
+theorem _root_.TopologicalSpace.IsSeparable.exists_countable_dense_subset
+   {s : Set α} (hs : IsSeparable s) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by
   have : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε := fun ε ε0 => by
     rcases hs with ⟨t, htc, hst⟩
     refine ⟨t, htc, hst.trans fun x hx => ?_⟩
     rcases mem_closure_iff.1 hx ε ε0 with ⟨y, hyt, hxy⟩
     exact mem_iUnion₂.2 ⟨y, hyt, mem_closedBall.2 hxy.le⟩
-  rcases subset_countable_closure_of_almost_dense_set _ this with ⟨t, hts, htc, hst⟩
+  exact subset_countable_closure_of_almost_dense_set _ this
+
+open TopologicalSpace in
+/-- 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 _root_.TopologicalSpace.IsSeparable.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 [inducing_subtype_val.dense_iff, Subtype.forall]

Mathlib/Topology/Separation.lean

@@ -410,6 +410,12 @@ theorem Ne.nhdsWithin_diff_singleton [T1Space α] {x y : α} (h : x ≠ y) (s :
   exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)
 #align ne.nhds_within_diff_singleton Ne.nhdsWithin_diff_singleton
 
+lemma nhdsWithin_compl_singleton_le [T1Space α] (x y : α) : 𝓝[{x}ᶜ] x ≤ 𝓝[{y}ᶜ] x := by
+  rcases eq_or_ne x y with rfl|hy
+  · exact Eq.le rfl
+  · rw [Ne.nhdsWithin_compl_singleton hy]
+    exact nhdsWithin_le_nhds
+
 theorem isOpen_setOf_eventually_nhdsWithin [T1Space α] {p : α → Prop} :
     IsOpen { x | ∀ᶠ y in 𝓝[≠] x, p y } := by
   refine' isOpen_iff_mem_nhds.mpr fun a ha => _