case intro
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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
ha : 0 < ↑a
h : ∀ (i : ι), i ∈ s → ↑(p i) x < ↑a
⊢ ↑(Finset.sup s p) x < ↑a
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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.le
case intro
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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
ha : 0 < ↑a
h : ∀ (i : ι), i ∈ s → ↑(p i) x < ↑a
⊢ ∀ (b : ι), b ∈ s → { val := ↑(p b) x, property := (_ : 0 ≤ ↑(p b) x) } < a

case intro
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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
ha : 0 < ↑a
h : ∀ (i : ι), i ∈ s → ↑(p i) x < ↑a
⊢ ⊥ < a
case intro
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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
ha : 0 < ↑a
h : ∀ (i : ι), i ∈ s → ↑(p i) x < ↑a
⊢ ↑(Finset.sup s p) x < ↑a
rw [finset_sup_apply, NNReal.coe_lt_coe, Finset.sup_lt_iff]
no goals
case intro
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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
ha : 0 < ↑a
h : ∀ (i : ι), i ∈ s → ↑(p i) x < ↑a
⊢ ∀ (b : ι), b ∈ s → { val := ↑(p b) x, property := (_ : 0 ≤ ↑(p b) x) } < a
exact h
no goals
case intro
R : Type ?u.528629
R' : Type ?u.528632
𝕜 : Type u_1
𝕜₂ : Type ?u.528638
𝕜₃ : Type ?u.528641
𝕝 : Type ?u.528644
E : Type u_2
E₂ : Type ?u.528650
E₃ : Type ?u.528653
F : Type ?u.528656
G : Type ?u.528659
ι : 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
ha : 0 < ↑a
h : ∀ (i : ι), i ∈ s → ↑(p i) x < ↑a
⊢ ⊥ < a
exact NNReal.coe_pos.mpr ha