𝕜 : Type u_3
𝕜₂ : Type ?u.18792
𝕝 : Type ?u.18795
𝕝₂ : Type ?u.18798
E : Type u_2
F : Type ?u.18804
G : Type ?u.18807
ι : Type u_1
ι' : Type ?u.18813
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ Set.Nonempty (basisSets p)
𝕜 : Type u_3
𝕜₂ : Type ?u.18792
𝕝 : Type ?u.18795
𝕝₂ : Type ?u.18798
E : Type u_2
F : Type ?u.18804
G : Type ?u.18807
ι : Type u_1
ι' : Type ?u.18813
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
⊢ Set.Nonempty (basisSets p)
let i := Classical.arbitrary ι
𝕜 : Type u_3
𝕜₂ : Type ?u.18792
𝕝 : Type ?u.18795
𝕝₂ : Type ?u.18798
E : Type u_2
F : Type ?u.18804
G : Type ?u.18807
ι : Type u_1
ι' : Type ?u.18813
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ ball (p i) 0 1 ∈ basisSets p
𝕜 : Type u_3
𝕜₂ : Type ?u.18792
𝕝 : Type ?u.18795
𝕝₂ : Type ?u.18798
E : Type u_2
F : Type ?u.18804
G : Type ?u.18807
ι : Type u_1
ι' : Type ?u.18813
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ Set.Nonempty (basisSets p)
refine' nonempty_def.mpr ⟨(p i).ball 0 1, _⟩
no goals
𝕜 : Type u_3
𝕜₂ : Type ?u.18792
𝕝 : Type ?u.18795
𝕝₂ : Type ?u.18798
E : Type u_2
F : Type ?u.18804
G : Type ?u.18807
ι : Type u_1
ι' : Type ?u.18813
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
i : ι := Classical.arbitrary ι
⊢ ball (p i) 0 1 ∈ basisSets p
exact p.basisSets_singleton_mem i zero_lt_one