no goals
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u
inst✝³ : TopologicalSpace A
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : TopologicalSemiring A
s : Subalgebra R A
⊢ IsClosed ↑(topologicalClosure s)
convert @isClosed_closure A _ s