case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.30056
𝕝 : Type ?u.30059
𝕝₂ : Type ?u.30062
E : Type u_1
F : Type ?u.30068
G : Type ?u.30071
ι : Type u_3
ι'✝ : Type ?u.30077
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup ι' p) 0 r
⊢ 0 ∈ U
𝕜 : Type u_2
𝕜₂ : Type ?u.30056
𝕝 : Type ?u.30059
𝕝₂ : Type ?u.30062
E : Type u_1
F : Type ?u.30068
G : Type ?u.30071
ι : Type u_3
ι' : Type ?u.30077
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU : U ∈ basisSets p
⊢ 0 ∈ U
rcases p.basisSets_iff.mp hU with ⟨ι', r, hr, hU⟩
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.30056
𝕝 : Type ?u.30059
𝕝₂ : Type ?u.30062
E : Type u_1
F : Type ?u.30068
G : Type ?u.30071
ι : Type u_3
ι'✝ : Type ?u.30077
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup ι' p) 0 r
⊢ 0 < r
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.30056
𝕝 : Type ?u.30059
𝕝₂ : Type ?u.30062
E : Type u_1
F : Type ?u.30068
G : Type ?u.30071
ι : Type u_3
ι'✝ : Type ?u.30077
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup ι' p) 0 r
⊢ 0 ∈ U
rw [hU, mem_ball_zero, map_zero]
no goals
case intro.intro.intro
𝕜 : Type u_2
𝕜₂ : Type ?u.30056
𝕝 : Type ?u.30059
𝕝₂ : Type ?u.30062
E : Type u_1
F : Type ?u.30068
G : Type ?u.30071
ι : Type u_3
ι'✝ : Type ?u.30077
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ basisSets p
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup ι' p) 0 r
⊢ 0 < r
exact hr