R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
H : BddAbove (FunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ ↑p x ≤ ↑(sSup s) x
R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
H : BddAbove (FunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ (fun f => ↑f) p x ≤ (fun f => ↑f) (sSup s) x
dsimp
R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
H : BddAbove (FunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
H : BddAbove (FunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ ↑p x ≤ ↑(sSup s) x
rw [Seminorm.coe_sSup_eq' H, iSup_apply]
case intro
R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
q : E → ℝ
hq : q ∈ upperBounds (FunLike.coe '' s)
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
H : BddAbove (FunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
rcases H with ⟨q, hq⟩
no goals
case intro
R : Type ?u.762821
R' : Type ?u.762824
𝕜 : Type u_2
𝕜₂ : Type ?u.762830
𝕜₃ : Type ?u.762833
𝕝 : Type ?u.762836
E : Type u_1
E₂ : Type ?u.762842
E₃ : Type ?u.762845
F : Type ?u.762848
G : Type ?u.762851
ι : Type ?u.762854
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p✝ q✝ : Seminorm 𝕜 E
x✝ : E
s : Set (Seminorm 𝕜 E)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
q : E → ℝ
hq : q ∈ upperBounds (FunLike.coe '' s)
⊢ ↑p x ≤ ⨆ (i : ↑s), ↑↑i x
exact
  le_ciSup ⟨q x, forall_range_iff.mpr fun i : s => hq (mem_image_of_mem _ i.2) x⟩ ⟨p, hp⟩