diff --git a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
index 9d8e84930a01b6..bec008e476e1a3 100644
--- a/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
+++ b/Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
@@ -950,12 +950,26 @@ theorem LinearMap.withSeminorms_induced {q : SeminormFamily 𝕜₂ F ι}
   refine iInf_congr fun i => ?_
   exact Filter.comap_comap
 
+protected theorem PolynormableSpace.induced [PolynormableSpace 𝕜₂ F] (f : E →ₛₗ[σ₁₂] F) :
+    PolynormableSpace 𝕜 E (topology := induced f inferInstance) := by
+  let _ : TopologicalSpace E := induced f inferInstance
+  exact f.withSeminorms_induced (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace
+
 lemma Topology.IsInducing.withSeminorms {q : SeminormFamily 𝕜₂ F ι}
     (hq : WithSeminorms q) [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
     WithSeminorms (q.comp f) := by
   rw [hf.eq_induced]
   exact f.withSeminorms_induced hq
 
+theorem Topology.IsInducing.polynormableSpace [PolynormableSpace 𝕜₂ F]
+    [TopologicalSpace E] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
+    PolynormableSpace 𝕜 E :=
+  hf.withSeminorms (PolynormableSpace.withSeminorms 𝕜₂ F) |>.toPolynormableSpace
+
+instance [PolynormableSpace 𝕜₂ F] {S : Submodule 𝕜₂ F} :
+    PolynormableSpace 𝕜₂ S :=
+  IsInducing.polynormableSpace (f := S.subtype) .subtypeVal
+
 /-- (Disjoint) union of seminorm families. -/
 protected def SeminormFamily.sigma {κ : ι → Type*} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) :
     SeminormFamily 𝕜 E ((i : ι) × κ i) :=
@@ -972,6 +986,25 @@ theorem withSeminorms_iInf {κ : ι → Type*}
   rw [iInf_sigma]
   exact iInf_congr hp
 
+theorem PolynormableSpace.iInf {t : ι → TopologicalSpace E}
+    (ht : ∀ i, PolynormableSpace 𝕜 E (topology := t i)) :
+    PolynormableSpace 𝕜 E (topology := ⨅ i, t i) := by
+  let _ : TopologicalSpace E := ⨅ i, t i
+  exact withSeminorms_iInf (fun i ↦ (ht i).withSeminorms') |>.toPolynormableSpace
+
+theorem PolynormableSpace.sInf {ts : Set (TopologicalSpace E)}
+    (hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E (topology := t)) :
+    PolynormableSpace 𝕜 E (topology := sInf ts) := by
+  rw [sInf_eq_iInf']
+  exact .iInf fun t ↦ hts t.1 t.2
+
+theorem PolynormableSpace.inf {t₁ t₂ : TopologicalSpace E}
+    (ht₁ : PolynormableSpace 𝕜 E (topology := t₁))
+    (ht₂ : PolynormableSpace 𝕜 E (topology := t₂)) :
+    PolynormableSpace 𝕜 E (topology := t₁ ⊓ t₂) := by
+  rw [← sInf_pair]
+  exact .sInf (by simp [ht₁, ht₂])
+
 theorem withSeminorms_pi {κ : ι → Type*} {E : ι → Type*}
     [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
     {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)}
@@ -979,6 +1012,16 @@ theorem withSeminorms_pi {κ : ι → Type*} {E : ι → Type*}
     WithSeminorms (SeminormFamily.sigma (fun i ↦ (p i).comp (LinearMap.proj i))) :=
   withSeminorms_iInf fun i ↦ (LinearMap.proj i).withSeminorms_induced (hp i)
 
+instance {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
+    [∀ i, TopologicalSpace (E i)] [∀ i, PolynormableSpace 𝕜 (E i)] :
+    PolynormableSpace 𝕜 (Π i, E i) :=
+  .iInf fun i ↦ .induced (LinearMap.proj (R := 𝕜) (φ := E) i)
+
+instance {E₁ E₂ : Type*} [AddCommGroup E₁] [AddCommGroup E₂] [Module 𝕜 E₁] [Module 𝕜 E₂]
+    [TopologicalSpace E₁] [TopologicalSpace E₂] [PolynormableSpace 𝕜 E₁] [PolynormableSpace 𝕜 E₂] :
+    PolynormableSpace 𝕜 (E₁ × E₂) :=
+  .inf (.induced <| LinearMap.fst 𝕜 E₁ E₂) (.induced <| LinearMap.snd 𝕜 E₁ E₂)
+
 end TopologicalConstructions
 
 section TopologicalProperties
diff --git a/Mathlib/Topology/Algebra/Module/LocallyConvex.lean b/Mathlib/Topology/Algebra/Module/LocallyConvex.lean
index dbbd09e50d5ea1..c888514e51ead3 100644
--- a/Mathlib/Topology/Algebra/Module/LocallyConvex.lean
+++ b/Mathlib/Topology/Algebra/Module/LocallyConvex.lean
@@ -197,6 +197,16 @@ protected theorem LocallyConvexSpace.induced {t : TopologicalSpace F} [LocallyCo
   rw [nhds_induced]
   exact (LocallyConvexSpace.convex_basis <| f x).comap f
 
+theorem Topology.IsInducing.locallyConvexSpace [TopologicalSpace F] [LocallyConvexSpace 𝕜 F]
+    [TopologicalSpace E] {f : E →ₗ[𝕜] F} (hf : IsInducing f) :
+    LocallyConvexSpace 𝕜 E := by
+  rw [hf.eq_induced]
+  exact .induced f
+
+instance [TopologicalSpace E] [LocallyConvexSpace 𝕜 E] {S : Submodule 𝕜 E} :
+    LocallyConvexSpace 𝕜 S :=
+  IsInducing.locallyConvexSpace (f := S.subtype) .subtypeVal
+
 instance Pi.locallyConvexSpace {ι : Type*} {X : ι → Type*} [∀ i, AddCommMonoid (X i)]
     [∀ i, TopologicalSpace (X i)] [∀ i, Module 𝕜 (X i)] [∀ i, LocallyConvexSpace 𝕜 (X i)] :
     LocallyConvexSpace 𝕜 (∀ i, X i) :=