𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
⊢ WithSeminorms (SeminormFamily.comp q f)
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
⊢ WithSeminorms (SeminormFamily.comp q f)
letI : TopologicalSpace E := induced f inferInstance
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this✝ : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
this : TopologicalAddGroup E := topologicalAddGroup_induced f
⊢ WithSeminorms (SeminormFamily.comp q f)
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
⊢ WithSeminorms (SeminormFamily.comp q f)
letI : TopologicalAddGroup E := topologicalAddGroup_induced f
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this✝ : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
this : TopologicalAddGroup E := topologicalAddGroup_induced f
⊢ (⨅ (i : ι), Filter.comap (↑f) (Filter.comap (↑(q i)) (𝓝 0))) =
    ⨅ (i : ι), Filter.comap (↑(SeminormFamily.comp q f i)) (𝓝 0)
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this✝ : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
this : TopologicalAddGroup E := topologicalAddGroup_induced f
⊢ WithSeminorms (SeminormFamily.comp q f)
rw [(q.comp f).withSeminorms_iff_nhds_eq_iInf, nhds_induced, map_zero,
  q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.comap_iInf]
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this✝ : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
this : TopologicalAddGroup E := topologicalAddGroup_induced f
i : ι
⊢ Filter.comap (↑f) (Filter.comap (↑(q i)) (𝓝 0)) = Filter.comap (↑(SeminormFamily.comp q f i)) (𝓝 0)
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this✝ : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
this : TopologicalAddGroup E := topologicalAddGroup_induced f
⊢ (⨅ (i : ι), Filter.comap (↑f) (Filter.comap (↑(q i)) (𝓝 0))) =
    ⨅ (i : ι), Filter.comap (↑(SeminormFamily.comp q f i)) (𝓝 0)
refine' iInf_congr fun i => _
no goals
𝕜 : Type u_4
𝕜₂ : Type u_2
𝕝 : Type ?u.715682
𝕝₂ : Type ?u.715685
E : Type u_5
F : Type u_3
G : Type ?u.715694
ι : Type u_1
ι' : Type ?u.715700
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
f : E →ₛₗ[σ₁₂] F
this✝ : TopologicalSpace E := TopologicalSpace.induced (↑f) inferInstance
this : TopologicalAddGroup E := topologicalAddGroup_induced f
i : ι
⊢ Filter.comap (↑f) (Filter.comap (↑(q i)) (𝓝 0)) = Filter.comap (↑(SeminormFamily.comp q f i)) (𝓝 0)
exact Filter.comap_comap