Dense spans

A generating family, regarded as a family in the closure of its span, has dense span there. This lets constructions on densely spanning families apply to arbitrary closed spans. Conversely, a densely spanning family stays densely spanning when pushed forward along a continuous linear map with dense range, such as the projection onto a quotient module, so that a quotient of a module spanned densely by a countable family is again spanned densely by one. No norm, separation, or completeness assumptions are needed.

theorem TauCeti.dense_span_in_topologicalClosure {R : Type u_1} {ι : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul R M] (v : ι → M) : Dense ↑(Submodule.span R (Set.range fun (i : ι) => ⟨v i, ⋯⟩))

A family of vectors in the closure of its span still has dense span there.

theorem DenseRange.dense_span_range_comp {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [TopologicalSpace M] [AddCommMonoid N] [Module R N] [TopologicalSpace N] {f : M →ₗ[R] N} (hf : DenseRange ⇑f) (hfc : Continuous ⇑f) {v : ι → M} (hv : Dense ↑(Submodule.span R (Set.range v))) : Dense ↑(Submodule.span R (Set.range (⇑f ∘ v)))

The image of a densely spanning family under a continuous linear map with dense range has dense span. For instance, the image of a densely spanning family in a quotient module M ⧸ p (take f = p.mkQ) has dense span.