𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)) id
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
⊢ WithSeminorms (gaugeSeminormFamily 𝕜 E)
refine' SeminormFamily.withSeminorms_of_hasBasis _ _
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
⊢ ∃ i', i' ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E) ∧ id i' ⊆ id s

case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)
⊢ ∃ i, (0 ∈ i ∧ IsOpen i ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)) id
refine' (nhds_basis_abs_convex_open 𝕜 E).to_hasBasis (fun s hs => _) fun s hs => _
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)
⊢ 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)
⊢ ∃ i, (0 ∈ i ∧ IsOpen i ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
refine' ⟨s, ⟨_, rfl.subset⟩⟩
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : ∃ i r x, s = Seminorm.ball (Finset.sup i (gaugeSeminormFamily 𝕜 E)) 0 r
⊢ 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)
⊢ 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
rw [SeminormFamily.basisSets_iff] at hs
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r ∧
    IsOpen (Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r) ∧
      Balanced 𝕜 (Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r) ∧
        Convex ℝ (Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r)
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : ∃ i r x, s = Seminorm.ball (Finset.sup i (gaugeSeminormFamily 𝕜 E)) 0 r
⊢ 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
rcases hs with ⟨t, r, hr, rfl⟩
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ (0 ∈ ⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r) ∧
    IsOpen (⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r) ∧
      Balanced 𝕜 (⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r) ∧
        Convex ℝ (⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r)
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ 0 ∈ Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r ∧
    IsOpen (Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r) ∧
      Balanced 𝕜 (Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r) ∧
        Convex ℝ (Seminorm.ball (Finset.sup t (gaugeSeminormFamily 𝕜 E)) 0 r)
rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
⊢ IsOpen (Seminorm.ball (gaugeSeminormFamily 𝕜 E S) 0 r)
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
⊢ (0 ∈ ⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r) ∧
    IsOpen (⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r) ∧
      Balanced 𝕜 (⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r) ∧
        Convex ℝ (⋂ (i : AbsConvexOpenSets 𝕜 E) (_ : i ∈ t), Seminorm.ball (gaugeSeminormFamily 𝕜 E i) 0 r)
refine'
  ⟨mem_iInter₂.mpr fun _ _ => by simp [Seminorm.mem_ball_zero, hr],
    isOpen_biInter (t.finite_toSet) fun S _ => _,
    balanced_iInter₂ fun _ _ => Seminorm.balanced_ball_zero _ _,
    convex_iInter₂ fun _ _ => Seminorm.convex_ball _ _ _⟩
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
⊢ IsOpen (Seminorm.ball (gaugeSeminormFamily 𝕜 E S) 0 r)
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
⊢ IsOpen (Seminorm.ball (gaugeSeminormFamily 𝕜 E S) 0 r)
have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen (Seminorm.ball (gaugeSeminormFamily 𝕜 E S) 0 r)
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
⊢ IsOpen (Seminorm.ball (gaugeSeminormFamily 𝕜 E S) 0 r)
have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen (↑r • ↑S)
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen (Seminorm.ball (gaugeSeminormFamily 𝕜 E S) 0 r)
rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
no goals
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
hr'' : ↑r ≠ 0
⊢ IsOpen (↑r • ↑S)
exact S.coe_isOpen.smul₀ hr''
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
⊢ s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
⊢ ∃ i', i' ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E) ∧ id i' ⊆ id s
refine' ⟨s, ⟨_, rfl.subset⟩⟩
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
⊢ s = Seminorm.ball (gaugeSeminormFamily 𝕜 E { val := s, property := hs }) 0 1
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
⊢ s ∈ SeminormFamily.basisSets (gaugeSeminormFamily 𝕜 E)
convert(gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
no goals
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
s : Set E
hs : 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s
⊢ s = Seminorm.ball (gaugeSeminormFamily 𝕜 E { val := s, property := hs }) 0 1
rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
x✝¹ : AbsConvexOpenSets 𝕜 E
x✝ : x✝¹ ∈ t
⊢ 0 ∈ Seminorm.ball (gaugeSeminormFamily 𝕜 E x✝¹) 0 r
simp [Seminorm.mem_ball_zero, hr]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
⊢ r = ‖↑r‖ * 1
simp [abs_of_pos hr]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.88243
G : Type ?u.88246
ι : Type ?u.88249
inst✝¹⁰ : IsROrC 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : IsScalarTower ℝ 𝕜 E
inst✝⁴ : ContinuousSMul ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
t : Finset (AbsConvexOpenSets 𝕜 E)
r : ℝ
hr : 0 < r
S : AbsConvexOpenSets 𝕜 E
x✝ : S ∈ fun i => i ∈ t.val
hr' : r = ‖↑r‖ * 1
⊢ ↑r ≠ 0
simp [hr.ne']