𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ WithSeminorms fun x => normSeminorm 𝕜 E
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ WithSeminorms fun x => normSeminorm 𝕜 E
let p : SeminormFamily 𝕜 E (Fin 1) := fun _ => normSeminorm 𝕜 E
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ 𝓝 0 = 𝓝 0
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ WithSeminorms fun x => normSeminorm 𝕜 E
refine'
  ⟨SeminormedAddCommGroup.toTopologicalAddGroup.ext
      p.addGroupFilterBasis.isTopologicalAddGroup _⟩
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun x => 0 < x) (Metric.ball 0)
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ 𝓝 0 = 𝓝 0
refine' Filter.HasBasis.eq_of_same_basis Metric.nhds_basis_ball _
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun x => 0 < x) (ball (normSeminorm 𝕜 E) 0)
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun x => 0 < x) (Metric.ball 0)
rw [← ball_normSeminorm 𝕜 E]
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ ∀ (i : Set E), i ∈ SeminormFamily.addGroupFilterBasis p → ∃ i', 0 < i' ∧ ball (normSeminorm 𝕜 E) 0 i' ⊆ id i
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun x => 0 < x) (ball (normSeminorm 𝕜 E) 0)
refine'
  Filter.HasBasis.to_hasBasis p.addGroupFilterBasis.nhds_zero_hasBasis _ fun r hr =>
    ⟨(normSeminorm 𝕜 E).ball 0 r, p.basisSets_singleton_mem 0 hr, rfl.subset⟩
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU : U ∈ SeminormFamily.basisSets p
⊢ ∃ i', 0 < i' ∧ ball (normSeminorm 𝕜 E) 0 i' ⊆ id U
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ ∀ (i : Set E), i ∈ SeminormFamily.addGroupFilterBasis p → ∃ i', 0 < i' ∧ ball (normSeminorm 𝕜 E) 0 i' ⊆ id i
rintro U (hU : U ∈ p.basisSets)
case intro.intro.intro
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ i', 0 < i' ∧ ball (normSeminorm 𝕜 E) 0 i' ⊆ id U
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU : U ∈ SeminormFamily.basisSets p
⊢ ∃ i', 0 < i' ∧ ball (normSeminorm 𝕜 E) 0 i' ⊆ id U
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
case intro.intro.intro
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ id U
case intro.intro.intro
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ∃ i', 0 < i' ∧ ball (normSeminorm 𝕜 E) 0 i' ⊆ id U
use r, hr
case intro.intro.intro
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ ball (Finset.sup s p) 0 r
case intro.intro.intro
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ id U
rw [hU, id.def]
case pos
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : Finset.Nonempty s
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ ball (Finset.sup s p) 0 r

case neg
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬Finset.Nonempty s
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ ball (Finset.sup s p) 0 r
case intro.intro.intro
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ ball (Finset.sup s p) 0 r
by_cases h : s.Nonempty
case neg
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬Finset.Nonempty s
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ univ
case neg
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬Finset.Nonempty s
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ ball (Finset.sup s p) 0 r
rw [Finset.not_nonempty_iff_eq_empty.mp h, Finset.sup_empty, ball_bot _ hr]
no goals
case neg
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : ¬Finset.Nonempty s
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ univ
exact Set.subset_univ _
no goals
case pos
𝕜✝ : Type ?u.457423
𝕜₂ : Type ?u.457426
𝕝 : Type ?u.457429
𝕝₂ : Type ?u.457432
E✝ : Type ?u.457435
F : Type ?u.457438
G : Type ?u.457441
ι : Type ?u.457444
ι' : Type ?u.457447
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ SeminormFamily.basisSets p
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = ball (Finset.sup s p) 0 r
h : Finset.Nonempty s
⊢ ball (normSeminorm 𝕜 E) 0 r ⊆ ball (Finset.sup s p) 0 r
rw [Finset.sup_const h]