case hbasis
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets p) id

case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Convex ℝ (id i)
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ LocallyConvexSpace ℝ E
apply ofBasisZero ℝ E id fun s => s ∈ p.basisSets
case hbasis
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (FilterBasis.filter AddGroupFilterBasis.toFilterBasis) (fun s => s ∈ SeminormFamily.basisSets p) id
case hbasis
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets p) id
rw [hp.1, AddGroupFilterBasis.nhds_eq _, AddGroupFilterBasis.N_zero]
no goals
case hbasis
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ Filter.HasBasis (FilterBasis.filter AddGroupFilterBasis.toFilterBasis) (fun s => s ∈ SeminormFamily.basisSets p) id
exact FilterBasis.hasBasis _
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
s : Set E
hs : s ∈ SeminormFamily.basisSets p
⊢ Convex ℝ (id s)
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ ∀ (i : Set E), i ∈ SeminormFamily.basisSets p → Convex ℝ (id i)
intro s hs
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
s : Set E
hs : s ∈ ⋃ (s : Finset ι) (r : ℝ) (_ : 0 < r), {ball (Finset.sup s p) 0 r}
⊢ Convex ℝ (id s)
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
s : Set E
hs : s ∈ SeminormFamily.basisSets p
⊢ Convex ℝ (id s)
change s ∈ Set.iUnion _ at hs
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
s : Set E
hs : ∃ i i_1 h, s = ball (Finset.sup i p) 0 i_1
⊢ Convex ℝ (id s)
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
s : Set E
hs : s ∈ ⋃ (s : Finset ι) (r : ℝ) (_ : 0 < r), {ball (Finset.sup s p) 0 r}
⊢ Convex ℝ (id s)
simp_rw [Set.mem_iUnion, Set.mem_singleton_iff] at hs
case hconvex.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
I : Finset ι
r : ℝ
w✝ : 0 < r
⊢ Convex ℝ (id (ball (Finset.sup I p) 0 r))
case hconvex
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
s : Set E
hs : ∃ i i_1 h, s = ball (Finset.sup i p) 0 i_1
⊢ Convex ℝ (id s)
rcases hs with ⟨I, r, _, rfl⟩
no goals
case hconvex.intro.intro.intro
𝕜 : Type u_1
𝕜₂ : Type ?u.678312
𝕝 : Type ?u.678315
𝕝₂ : Type ?u.678318
E : Type u_2
F : Type ?u.678324
G : Type ?u.678327
ι : Type u_3
ι' : Type ?u.678333
inst✝⁸ : Nonempty ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedSpace ℝ 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module ℝ E
inst✝² : IsScalarTower ℝ 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
I : Finset ι
r : ℝ
w✝ : 0 < r
⊢ Convex ℝ (id (ball (Finset.sup I p) 0 r))
exact convex_ball _ _ _