Theorem: DenseRange.topologicalClosure_map_submodule' (DividedPowers/ForMathlib/Topology/Algebra/Algebra/Basic.lean)

State before:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : s.topologicalClosure = ⊤
⊢ (Submodule.map (↑f) s).topologicalClosure = ⊤
Tactic:
rw [SetLike.ext'_iff] at hs ⊢
State after:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤

State before:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Submodule.map (↑f) s).topologicalClosure = ↑⊤
Tactic:
simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢
State after:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : Dense ↑s
⊢ Dense ↑(Submodule.map (↑f) s)

State before:
R : Type u_1
inst✝¹³ : CommSemiring R
inst✝¹² : TopologicalSpace R
inst✝¹¹ : TopologicalSemiring R
A : Type u_2
inst✝¹⁰ : Semiring A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : TopologicalSemiring A
B : Type u_3
inst✝⁷ : Semiring B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : TopologicalSpace R
inst✝² : ContinuousAdd A
inst✝¹ : ContinuousSMul R B
inst✝ : ContinuousAdd B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Submodule R A
hs : Dense ↑s
⊢ Dense ↑(Submodule.map (↑f) s)
Tactic:
exact hf'.dense_image f.continuous hs
State after:
no goals