case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU : U ∈ basisSets p
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ {x | x • v ∈ ball (Finset.sup s p) 0 r} ∈ 𝓝 0
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U
rw [hU, Filter.eventually_iff]
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ {x | ‖x‖ * ↑(Finset.sup s p) v < r} ∈ 𝓝 0
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ {x | x • v ∈ ball (Finset.sup s p) 0 r} ∈ 𝓝 0
simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul]
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : 0 < ↑(Finset.sup s p) v
⊢ {x | ‖x‖ * ↑(Finset.sup s p) v < r} ∈ 𝓝 0

case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬0 < ↑(Finset.sup s p) v
⊢ {x | ‖x‖ * ↑(Finset.sup s p) v < r} ∈ 𝓝 0
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ {x | ‖x‖ * ↑(Finset.sup s p) v < r} ∈ 𝓝 0
by_cases h : 0 < (s.sup p) v
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬0 < ↑(Finset.sup s p) v
⊢ {x | True} ∈ 𝓝 0
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬0 < ↑(Finset.sup s p) v
⊢ {x | ‖x‖ * ↑(Finset.sup s p) v < r} ∈ 𝓝 0
simp_rw [le_antisymm (not_lt.mp h) (map_nonneg _ v), MulZeroClass.mul_zero, hr]
no goals
case neg
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬0 < ↑(Finset.sup s p) v
⊢ {x | True} ∈ 𝓝 0
exact IsOpen.mem_nhds isOpen_univ (mem_univ 0)
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : 0 < ↑(Finset.sup s p) v
⊢ {x | ‖x‖ < r / ↑(Finset.sup s p) v} ∈ 𝓝 0
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : 0 < ↑(Finset.sup s p) v
⊢ {x | ‖x‖ * ↑(Finset.sup s p) v < r} ∈ 𝓝 0
simp_rw [(lt_div_iff h).symm]
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : 0 < ↑(Finset.sup s p) v
⊢ Metric.ball 0 (r / ↑(Finset.sup s p) v) ∈ 𝓝 0
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : 0 < ↑(Finset.sup s p) v
⊢ {x | ‖x‖ < r / ↑(Finset.sup s p) v} ∈ 𝓝 0
rw [← _root_.ball_zero_eq]
no goals
case pos
𝕜 : Type u_2
𝕜₂ : Type ?u.53503
𝕝 : Type ?u.53506
𝕝₂ : Type ?u.53509
E : Type u_1
F : Type ?u.53515
G : Type ?u.53518
ι : Type u_3
ι' : Type ?u.53524
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
v : E
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : 0 < ↑(Finset.sup s p) v
⊢ Metric.ball 0 (r / ↑(Finset.sup s p) v) ∈ 𝓝 0
exact Metric.ball_mem_nhds 0 (div_pos hr h)