English
If f has dense range and S is a submodule of the domain with closure equal to the whole space, then the image submodule has dense closure in the codomain: (f(S)) closure = codomain.
Русский
Пусть f имеет плотный образ и подмодуль S домена имеет замыкание, равное всему пространству. Тогда образ S имеет плотное замыкание в кодомодуля:
LaTeX
$$$ \overline{f(S)} = M_2. $$$$
Lean4
/-- Under a dense continuous linear map, a submodule whose `TopologicalClosure` is `⊤` is sent to
another such submodule. That is, the image of a dense set under a map with dense range is dense.
-/
theorem _root_.DenseRange.topologicalClosure_map_submodule [RingHomSurjective σ₁₂] [TopologicalSpace R₁]
[TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] [ContinuousSMul R₂ M₂] [ContinuousAdd M₂]
{f : M₁ →SL[σ₁₂] M₂} (hf' : DenseRange f) {s : Submodule R₁ M₁} (hs : s.topologicalClosure = ⊤) :
(s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure = ⊤ :=
by
rw [SetLike.ext'_iff] at hs ⊢
simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢
exact hf'.dense_image f.continuous hs
