𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r) ↔
    ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
rw [hp.isVonNBounded_iff_finset_seminorm_bounded]
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r) →
    ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r

case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r) →
    ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r) ↔
    ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
constructor
case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r) →
    ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
intro hi I
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
hI : Finset.Nonempty I
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r

case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
hI : ¬Finset.Nonempty I
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
by_cases hI : I.Nonempty
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
hI : ¬Finset.Nonempty I
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → 0 < r
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
hI : ¬Finset.Nonempty I
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
simp only [Finset.not_nonempty_iff_eq_empty.mp hI, Finset.sup_empty, coe_bot, Pi.zero_apply,
  exists_prop]
no goals
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
hI : ¬Finset.Nonempty I
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → 0 < r
exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
i : ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r) →
    ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
intro hI i
case h.e'_2.h.h.e'_2.h.h'.h.e'_3.h.e'_5
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
i : ι
x✝ : ℝ
a✝¹ : E
a✝ : a✝¹ ∈ s
⊢ p i = Finset.sup {i} p
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
i : ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
convert hI {i}
no goals
case h.e'_2.h.h.e'_2.h.h'.h.e'_3.h.e'_5
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
i : ι
x✝ : ℝ
a✝¹ : E
a✝ : a✝¹ ∈ s
⊢ p i = Finset.sup {i} p
rw [Finset.sup_singleton]
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(p i) x < r
I : Finset ι
hI : Finset.Nonempty I
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
choose r hr h using hi
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
have h' : 0 < I.sup' hI r := by
  rcases hI.bex with ⟨i, hi⟩
  exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ↑(p i) x < Finset.sup' I hI r
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
refine' ⟨I.sup' hI r, h', fun x hx => finset_sup_apply_lt h' fun i hi => _⟩
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ r i ≤ Finset.sup' I hI r
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ↑(p i) x < Finset.sup' I hI r
refine' lt_of_lt_of_le (h i x hx) _
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ∃ b, b ∈ I ∧ r i ≤ r b
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ r i ≤ Finset.sup' I hI r
simp only [Finset.le_sup'_iff, exists_prop]
no goals
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
h' : 0 < Finset.sup' I hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ∃ b, b ∈ I ∧ r i ≤ r b
exact ⟨i, hi, (Eq.refl _).le⟩
case intro
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
i : ι
hi : i ∈ I
⊢ 0 < Finset.sup' I hI r
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
⊢ 0 < Finset.sup' I hI r
rcases hI.bex with ⟨i, hi⟩
no goals
case intro
𝕜 : Type u_2
𝕜₂ : Type ?u.478584
𝕝 : Type ?u.478587
𝕝₂ : Type ?u.478590
E : Type u_1
F : Type ?u.478596
G : Type ?u.478599
ι : Type u_3
ι' : Type ?u.478605
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : Finset.Nonempty I
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι) (x : E), x ∈ s → ↑(p i) x < r i
i : ι
hi : i ∈ I
⊢ 0 < Finset.sup' I hI r
exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)