English
If a subset s of a topological R-module M is separable and R is a separable ring, then the R-span of s is also separable in M.
Русский
Пусть S ⊆ M сепарабелен в топологическом R-модуле M, и R — сепарабельное кольцо; тогда линейная оболочка S над R сепарабельна.
LaTeX
$$$\text{IsSeparable}(s) \Rightarrow \text{IsSeparable}(\operatorname{span}_R s).$$$
Lean4
/-- The span of a separable subset with respect to a separable scalar ring is again separable. -/
theorem 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 [Submodule.span_eq_iUnion_nat]
refine .iUnion fun n ↦ .image ?_ ?_
· have : IsSeparable {f : Fin n → R × M | ∀ (i : Fin n), f i ∈ Set.univ ×ˢ s} := by
apply isSeparable_pi (fun i ↦ .prod (.of_separableSpace Set.univ) hs)
rwa [Set.univ_prod] at this
· apply continuous_finset_sum _ (fun i _ ↦ ?_)
exact (continuous_fst.comp (continuous_apply i)).smul (continuous_snd.comp (continuous_apply i))
