case h
𝕜 : Type u_4
𝕜₂ : Type u_1
𝕝 : Type ?u.705364
𝕝₂ : Type ?u.705367
E : Type u_5
F : Type u_2
G : Type ?u.705376
ι : Type u_3
ι' : Type ?u.705382
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(Seminorm.comp (Finset.sup s q) f) x = ↑(Finset.sup s (comp q f)) x
𝕜 : Type u_4
𝕜₂ : Type u_1
𝕝 : Type ?u.705364
𝕝₂ : Type ?u.705367
E : Type u_5
F : Type u_2
G : Type ?u.705376
ι : Type u_3
ι' : Type ?u.705382
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
⊢ Seminorm.comp (Finset.sup s q) f = Finset.sup s (comp q f)
ext x
case h
𝕜 : Type u_4
𝕜₂ : Type u_1
𝕝 : Type ?u.705364
𝕝₂ : Type ?u.705367
E : Type u_5
F : Type u_2
G : Type ?u.705376
ι : Type u_3
ι' : Type ?u.705382
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(Finset.sup s fun i => { val := ↑(q i) (↑f x), property := (_ : 0 ≤ ↑(q i) (↑f x)) }) =
    ↑(Finset.sup s fun i => { val := ↑(comp q f i) x, property := (_ : 0 ≤ ↑(comp q f i) x) })
case h
𝕜 : Type u_4
𝕜₂ : Type u_1
𝕝 : Type ?u.705364
𝕝₂ : Type ?u.705367
E : Type u_5
F : Type u_2
G : Type ?u.705376
ι : Type u_3
ι' : Type ?u.705382
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(Seminorm.comp (Finset.sup s q) f) x = ↑(Finset.sup s (comp q f)) x
rw [Seminorm.comp_apply, Seminorm.finset_sup_apply, Seminorm.finset_sup_apply]
no goals
case h
𝕜 : Type u_4
𝕜₂ : Type u_1
𝕝 : Type ?u.705364
𝕝₂ : Type ?u.705367
E : Type u_5
F : Type u_2
G : Type ?u.705376
ι : Type u_3
ι' : Type ?u.705382
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : NormedField 𝕜₂
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
q : SeminormFamily 𝕜₂ F ι
s : Finset ι
f : E →ₛₗ[σ₁₂] F
x : E
⊢ ↑(Finset.sup s fun i => { val := ↑(q i) (↑f x), property := (_ : 0 ≤ ↑(q i) (↑f x)) }) =
    ↑(Finset.sup s fun i => { val := ↑(comp q f i) x, property := (_ : 0 ≤ ↑(comp q f i) x) })
rfl