𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s) ↔
    ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
rw [hp.hasBasis.isVonNBounded_basis_iff]
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s) →
    ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r

case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s) ↔
    ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
constructor
case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs' : s' ∈ SeminormFamily.basisSets p
⊢ Absorbs 𝕜 (id s') s
case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s
intro h s' hs'
case mpr.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
⊢ Absorbs 𝕜 (id s') s
case mpr
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs' : s' ∈ SeminormFamily.basisSets p
⊢ Absorbs 𝕜 (id s') s
rcases p.basisSets_iff.mp hs' with ⟨I, r, hr, hs'⟩
case mpr.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) s
case mpr.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
⊢ Absorbs 𝕜 (id s') s
rw [id.def, hs']
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r'
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) s
case mpr.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) s
rcases h I with ⟨r', _, h'⟩
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ (x : E), x ∈ s → x ∈ ball (Finset.sup I p) 0 r'
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) s
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r'
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) s
simp_rw [← (I.sup p).mem_ball_zero] at h'
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ (x : E), x ∈ s → x ∈ ball (Finset.sup I p) 0 r'
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) (ball (Finset.sup I p) 0 r')
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ (x : E), x ∈ s → x ∈ ball (Finset.sup I p) 0 r'
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) s
refine' Absorbs.mono_right _ h'
no goals
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
s' : Set E
hs'✝ : s' ∈ SeminormFamily.basisSets p
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = ball (Finset.sup I p) 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ (x : E), x ∈ s → x ∈ ball (Finset.sup I p) 0 r'
⊢ Absorbs 𝕜 (ball (Finset.sup I p) 0 r) (ball (Finset.sup I p) 0 r')
exact (Finset.sup I p).ball_zero_absorbs_ball_zero hr
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s
I : Finset ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s) →
    ∀ (I : Finset ι), ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
intro h I
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 i s
I : Finset ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 (id i) s
I : Finset ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
simp only [id.def] at h
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h : Absorbs 𝕜 (ball (Finset.sup I p) 0 1) s
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
h : ∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Absorbs 𝕜 i s
I : Finset ι
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
specialize h ((I.sup p).ball 0 1) (p.basisSets_mem I zero_lt_one)
case mp.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → s ⊆ a • ball (Finset.sup I p) 0 1
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
h : Absorbs 𝕜 (ball (Finset.sup I p) 0 1) s
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
rcases h with ⟨r, hr, h⟩
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → s ⊆ a • ball (Finset.sup I p) 0 1
a : 𝕜
ha : r < ‖a‖
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → s ⊆ a • ball (Finset.sup I p) 0 1
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
cases' NormedField.exists_lt_norm 𝕜 r with a ha
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ a • ball (Finset.sup I p) 0 1
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → s ⊆ a • ball (Finset.sup I p) 0 1
a : 𝕜
ha : r < ‖a‖
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
specialize h a (le_of_lt ha)
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ ball (Finset.sup I p) 0 ‖a‖
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ a • ball (Finset.sup I p) 0 1
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ ball (Finset.sup I p) 0 ‖a‖
⊢ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < ‖a‖
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ ball (Finset.sup I p) 0 ‖a‖
⊢ ∃ r, r > 0 ∧ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < r
refine' ⟨‖a‖, lt_trans hr ha, _⟩
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ ball (Finset.sup I p) 0 ‖a‖
x : E
hx : x ∈ s
⊢ ↑(Finset.sup I p) x < ‖a‖
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ ball (Finset.sup I p) 0 ‖a‖
⊢ ∀ (x : E), x ∈ s → ↑(Finset.sup I p) x < ‖a‖
intro x hx
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
x : E
hx : x ∈ s
h : x ∈ ball (Finset.sup I p) 0 ‖a‖
⊢ ↑(Finset.sup I p) x < ‖a‖
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
h : s ⊆ ball (Finset.sup I p) 0 ‖a‖
x : E
hx : x ∈ s
⊢ ↑(Finset.sup I p) x < ‖a‖
specialize h hx
no goals
case mp.intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.464932
𝕝 : Type ?u.464935
𝕝₂ : Type ?u.464938
E : Type u_1
F : Type ?u.464944
G : Type ?u.464947
ι : Type u_3
ι' : Type ?u.464953
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 : ℝ
hr : 0 < r
a : 𝕜
ha : r < ‖a‖
x : E
hx : x ∈ s
h : x ∈ ball (Finset.sup I p) 0 ‖a‖
⊢ ↑(Finset.sup I p) x < ‖a‖
exact (Finset.sup I p).mem_ball_zero.mp h