𝕜 : Type u_5
𝕜₂ : Type u_2
𝕝 : Type ?u.841276
𝕝₂ : Type ?u.841279
E : Type u_4
F : Type u_3
G : Type ?u.841288
ι : Type u_1
ι' : Type ?u.841294
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
hι : Nonempty ι
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : Inducing ↑f
⊢ WithSeminorms (SeminormFamily.comp q f)
𝕜 : Type u_5
𝕜₂ : Type u_2
𝕝 : Type ?u.841276
𝕝₂ : Type ?u.841279
E : Type u_4
F : Type u_3
G : Type ?u.841288
ι : Type u_1
ι' : Type ?u.841294
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
hι : Nonempty ι
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : Inducing ↑f
⊢ WithSeminorms (SeminormFamily.comp q f)
rw [hf.induced]
no goals
𝕜 : Type u_5
𝕜₂ : Type u_2
𝕝 : Type ?u.841276
𝕝₂ : Type ?u.841279
E : Type u_4
F : Type u_3
G : Type ?u.841288
ι : Type u_1
ι' : Type ?u.841294
inst✝⁹ : NormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : NormedField 𝕜₂
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝³ : RingHomIsometric σ₁₂
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
hι : Nonempty ι
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst✝ : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : Inducing ↑f
⊢ WithSeminorms (SeminormFamily.comp q f)
exact f.withSeminorms_induced hq