Balanced.mulActionHom_preimage

Mathlib/Analysis/LocallyConvex/Basic.lean

@@ -42,7 +42,7 @@ open Set
 
 open Pointwise Topology
 
-variable {𝕜 𝕝 E : Type*} {ι : Sort*} {κ : ι → Sort*}
+variable {𝕜 𝕝 E F : Type*} {ι : Sort*} {κ : ι → Sort*}
 
 section SeminormedRing
 
@@ -105,6 +105,11 @@ theorem balanced_iInter₂ {f : ∀ i, κ i → Set E} (h : ∀ i j, Balanced 
     Balanced 𝕜 (⋂ (i) (j), f i j) :=
   balanced_iInter fun _ => balanced_iInter <| h _
 
+theorem Balanced.mulActionHom_preimage [SMul 𝕜 F] {s : Set F} (hs : Balanced 𝕜 s)
+    (f : MulActionHom (RingHom.id 𝕜) E  F) : Balanced 𝕜 (f ⁻¹' s) := fun a ha x ⟨y,⟨hy₁,hy₂⟩⟩ => by
+  rw [mem_preimage, ← hy₂, map_smul]
+  exact hs a ha (smul_mem_smul_set hy₁)
+
 variable [SMul 𝕝 E] [SMulCommClass 𝕜 𝕝 E]
 
 theorem Balanced.smul (a : 𝕝) (hs : Balanced 𝕜 s) : Balanced 𝕜 (a • s) := fun _b hb =>