case intro
R : Type ?u.518585
R' : Type ?u.518588
𝕜 : Type u_1
𝕜₂ : Type ?u.518594
𝕜₃ : Type ?u.518597
𝕝 : Type ?u.518600
E : Type u_2
E₂ : Type ?u.518606
E₃ : Type ?u.518609
F : Type ?u.518612
G : Type ?u.518615
ι : Type u_3
inst✝¹⁸ : SeminormedRing 𝕜
inst✝¹⁷ : SeminormedRing 𝕜₂
inst✝¹⁶ : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁴ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹³ : RingHomIsometric σ₁₃
inst✝¹² : AddCommGroup E
inst✝¹¹ : AddCommGroup E₂
inst✝¹⁰ : AddCommGroup E₃
inst✝⁹ : AddCommGroup F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜₂ E₂
inst✝⁵ : Module 𝕜₃ E₃
inst✝⁴ : Module 𝕜 F
inst✝³ : Module 𝕜 G
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ (i : ι), i ∈ s → ↑(p i) x ≤ ↑a
⊢ ↑(Finset.sup s p) x ≤ ↑a
R : Type ?u.518585
R' : Type ?u.518588
𝕜 : Type u_1
𝕜₂ : Type ?u.518594
𝕜₃ : Type ?u.518597
𝕝 : Type ?u.518600
E : Type u_2
E₂ : Type ?u.518606
E₃ : Type ?u.518609
F : Type ?u.518612
G : Type ?u.518615
ι : Type u_3
inst✝¹⁸ : SeminormedRing 𝕜
inst✝¹⁷ : SeminormedRing 𝕜₂
inst✝¹⁶ : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁴ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹³ : RingHomIsometric σ₁₃
inst✝¹² : AddCommGroup E
inst✝¹¹ : AddCommGroup E₂
inst✝¹⁰ : AddCommGroup E₃
inst✝⁹ : AddCommGroup F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜₂ E₂
inst✝⁵ : Module 𝕜₃ E₃
inst✝⁴ : Module 𝕜 F
inst✝³ : Module 𝕜 G
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ
ha : 0 ≤ a
h : ∀ (i : ι), i ∈ s → ↑(p i) x ≤ a
⊢ ↑(Finset.sup s p) x ≤ a
lift a to ℝ≥0 using ha
case intro
R : Type ?u.518585
R' : Type ?u.518588
𝕜 : Type u_1
𝕜₂ : Type ?u.518594
𝕜₃ : Type ?u.518597
𝕝 : Type ?u.518600
E : Type u_2
E₂ : Type ?u.518606
E₃ : Type ?u.518609
F : Type ?u.518612
G : Type ?u.518615
ι : Type u_3
inst✝¹⁸ : SeminormedRing 𝕜
inst✝¹⁷ : SeminormedRing 𝕜₂
inst✝¹⁶ : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁴ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹³ : RingHomIsometric σ₁₃
inst✝¹² : AddCommGroup E
inst✝¹¹ : AddCommGroup E₂
inst✝¹⁰ : AddCommGroup E₃
inst✝⁹ : AddCommGroup F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜₂ E₂
inst✝⁵ : Module 𝕜₃ E₃
inst✝⁴ : Module 𝕜 F
inst✝³ : Module 𝕜 G
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ (i : ι), i ∈ s → ↑(p i) x ≤ ↑a
⊢ (Finset.sup s fun i => { val := ↑(p i) x, property := (_ : 0 ≤ ↑(p i) x) }) ≤ a
case intro
R : Type ?u.518585
R' : Type ?u.518588
𝕜 : Type u_1
𝕜₂ : Type ?u.518594
𝕜₃ : Type ?u.518597
𝕝 : Type ?u.518600
E : Type u_2
E₂ : Type ?u.518606
E₃ : Type ?u.518609
F : Type ?u.518612
G : Type ?u.518615
ι : Type u_3
inst✝¹⁸ : SeminormedRing 𝕜
inst✝¹⁷ : SeminormedRing 𝕜₂
inst✝¹⁶ : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁴ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹³ : RingHomIsometric σ₁₃
inst✝¹² : AddCommGroup E
inst✝¹¹ : AddCommGroup E₂
inst✝¹⁰ : AddCommGroup E₃
inst✝⁹ : AddCommGroup F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜₂ E₂
inst✝⁵ : Module 𝕜₃ E₃
inst✝⁴ : Module 𝕜 F
inst✝³ : Module 𝕜 G
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ (i : ι), i ∈ s → ↑(p i) x ≤ ↑a
⊢ ↑(Finset.sup s p) x ≤ ↑a
rw [finset_sup_apply, NNReal.coe_le_coe]
no goals
case intro
R : Type ?u.518585
R' : Type ?u.518588
𝕜 : Type u_1
𝕜₂ : Type ?u.518594
𝕜₃ : Type ?u.518597
𝕝 : Type ?u.518600
E : Type u_2
E₂ : Type ?u.518606
E₃ : Type ?u.518609
F : Type ?u.518612
G : Type ?u.518615
ι : Type u_3
inst✝¹⁸ : SeminormedRing 𝕜
inst✝¹⁷ : SeminormedRing 𝕜₂
inst✝¹⁶ : SeminormedRing 𝕜₃
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝¹⁵ : RingHomIsometric σ₁₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
inst✝¹⁴ : RingHomIsometric σ₂₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝¹³ : RingHomIsometric σ₁₃
inst✝¹² : AddCommGroup E
inst✝¹¹ : AddCommGroup E₂
inst✝¹⁰ : AddCommGroup E₃
inst✝⁹ : AddCommGroup F
inst✝⁸ : AddCommGroup G
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜₂ E₂
inst✝⁵ : Module 𝕜₃ E₃
inst✝⁴ : Module 𝕜 F
inst✝³ : Module 𝕜 G
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
a : ℝ≥0
h : ∀ (i : ι), i ∈ s → ↑(p i) x ≤ ↑a
⊢ (Finset.sup s fun i => { val := ↑(p i) x, property := (_ : 0 ≤ ↑(p i) x) }) ≤ a
exact Finset.sup_le h