case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU : U ∈ basisSets p
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ Metric.ball 0 (Real.sqrt r) • W ⊆ U
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
refine' ⟨Metric.ball 0 r.sqrt, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), _⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ Metric.ball 0 (Real.sqrt r) • ball (Finset.sup s p) 0 (Real.sqrt r) ⊆ U
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ Metric.ball 0 (Real.sqrt r) • W ⊆ U
refine' ⟨(s.sup p).ball 0 r.sqrt, p.basisSets_mem s (Real.sqrt_pos.mpr hr), _⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) 0 (Real.sqrt r * Real.sqrt r) ⊆ U
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ Metric.ball 0 (Real.sqrt r) • ball (Finset.sup s p) 0 (Real.sqrt r) ⊆ U
refine' Set.Subset.trans (ball_smul_ball (s.sup p) r.sqrt r.sqrt) _
no goals
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.63334
𝕝 : Type ?u.63337
𝕝₂ : Type ?u.63340
E : Type u_1
F : Type ?u.63346
G : Type ?u.63349
ι : Type u_3
ι' : Type ?u.63355
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
U : Set E
hU✝ : U ∈ basisSets p
s : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (Finset.sup s p) 0 (Real.sqrt r * Real.sqrt r) ⊆ U
rw [hU, Real.mul_self_sqrt (le_of_lt hr)]