[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
x : E
⊢ x ∈ balancedCore 𝕜 s ↔ ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ x ∈ t
[PROOFSTEP]
simp_rw [balancedCore, mem_sUnion, mem_setOf_eq, and_assoc]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedCore 𝕜 s ⊆ balancedCore 𝕜 s
[PROOFSTEP]
rintro x ⟨y, hy, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCore 𝕜 s
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
[PROOFSTEP]
rw [mem_balancedCore_iff] at hy
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∃ t, Balanced 𝕜 t ∧ t ⊆ s ∧ y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
[PROOFSTEP]
rcases hy with ⟨t, ht1, ht2, hy⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ : Set E
x : E
s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
t : Set E
ht1 : Balanced 𝕜 t
ht2 : t ⊆ s
hy : y ∈ t
⊢ (fun x => a • x) y ∈ balancedCore 𝕜 s
[PROOFSTEP]
exact ⟨t, ⟨ht1, ht2⟩, ht1 a ha (smul_mem_smul_set hy)⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
x : E
ht : Balanced 𝕜 t
h : s ⊆ t
⊢ balancedHull 𝕜 s ⊆ t
[PROOFSTEP]
intros x hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
x✝ : E
ht : Balanced 𝕜 t
h : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ t
[PROOFSTEP]
obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 hx
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
x : E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun x => r • x) y ∈ balancedHull 𝕜 s
⊢ (fun x => r • x) y ∈ t
[PROOFSTEP]
exact ht.smul_mem hr (h hy)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
⊢ Balanced 𝕜 (balancedHull 𝕜 s)
[PROOFSTEP]
intro a ha
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • balancedHull 𝕜 s ⊆ balancedHull 𝕜 s
[PROOFSTEP]
simp_rw [balancedHull, smul_set_iUnion₂, subset_def, mem_iUnion₂]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ ∀ (x : E), (∃ i j, x ∈ a • i • s) → ∃ i j, x ∈ i • s
[PROOFSTEP]
rintro x ⟨r, hr, hx⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx : x ∈ a • r • s
⊢ ∃ i j, x ∈ i • s
[PROOFSTEP]
rw [← smul_assoc] at hx
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ s : Set E
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
r : 𝕜
hr : ‖r‖ ≤ 1
hx✝ : x ∈ a • r • s
hx : x ∈ (a • r) • s
⊢ ∃ i j, x ∈ i • s
[PROOFSTEP]
exact ⟨a • r, (SeminormedRing.norm_mul _ _).trans (mul_le_one ha (norm_nonneg r) hr), hx⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ balancedCoreAux 𝕜 ∅ = ∅
[PROOFSTEP]
simp_rw [balancedCoreAux, iInter₂_eq_empty_iff, smul_set_empty]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
⊢ ∀ (a : E), ∃ i h, ¬a ∈ ∅
[PROOFSTEP]
exact fun _ => ⟨1, norm_one.ge, not_mem_empty _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
x : E
hx : x ∈ balancedCoreAux 𝕜 s
⊢ x ∈ s
[PROOFSTEP]
simpa only [one_smul] using mem_balancedCoreAux_iff.1 hx 1 norm_one.ge
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
⊢ Balanced 𝕜 (balancedCoreAux 𝕜 s)
[PROOFSTEP]
rintro a ha x ⟨y, hy, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
⊢ (fun x => a • x) y ∈ balancedCoreAux 𝕜 s
[PROOFSTEP]
obtain rfl | h := eq_or_ne a 0
[GOAL]
case intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
y : E
hy : y ∈ balancedCoreAux 𝕜 s
ha : ‖0‖ ≤ 1
⊢ (fun x => 0 • x) y ∈ balancedCoreAux 𝕜 s
[PROOFSTEP]
simp_rw [zero_smul, h0]
[GOAL]
case intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : y ∈ balancedCoreAux 𝕜 s
h : a ≠ 0
⊢ (fun x => a • x) y ∈ balancedCoreAux 𝕜 s
[PROOFSTEP]
rw [mem_balancedCoreAux_iff] at hy ⊢
[GOAL]
case intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
⊢ ∀ (r : 𝕜), 1 ≤ ‖r‖ → (fun x => a • x) y ∈ r • s
[PROOFSTEP]
intro r hr
[GOAL]
case intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ (fun x => a • x) y ∈ r • s
[PROOFSTEP]
have h'' : 1 ≤ ‖a⁻¹ • r‖ := by
  rw [norm_smul, norm_inv]
  exact one_le_mul_of_one_le_of_one_le (one_le_inv (norm_pos_iff.mpr h) ha) hr
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a⁻¹ • r‖
[PROOFSTEP]
rw [norm_smul, norm_inv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ 1 ≤ ‖a‖⁻¹ * ‖r‖
[PROOFSTEP]
exact one_le_mul_of_one_le_of_one_le (one_le_inv (norm_pos_iff.mpr h) ha) hr
[GOAL]
case intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
⊢ (fun x => a • x) y ∈ r • s
[PROOFSTEP]
have h' := hy (a⁻¹ • r) h''
[GOAL]
case intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h0 : 0 ∈ balancedCoreAux 𝕜 s
a : 𝕜
ha : ‖a‖ ≤ 1
y : E
hy : ∀ (r : 𝕜), 1 ≤ ‖r‖ → y ∈ r • s
h : a ≠ 0
r : 𝕜
hr : 1 ≤ ‖r‖
h'' : 1 ≤ ‖a⁻¹ • r‖
h' : y ∈ (a⁻¹ • r) • s
⊢ (fun x => a • x) y ∈ r • s
[PROOFSTEP]
rwa [smul_assoc, mem_inv_smul_set_iff₀ h] at h'
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
⊢ t ⊆ balancedCoreAux 𝕜 s
[PROOFSTEP]
refine' fun x hx => mem_balancedCoreAux_iff.2 fun r hr => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ x ∈ r • s
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp <| zero_lt_one.trans_le hr)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ r⁻¹ • x ∈ s
[PROOFSTEP]
refine' h (ht.smul_mem _ hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
h : t ⊆ s
ht : Balanced 𝕜 t
x : E
hx : x ∈ t
r : 𝕜
hr : 1 ≤ ‖r‖
⊢ ‖r‖⁻¹ ≤ 1
[PROOFSTEP]
exact inv_le_one hr
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ balancedCore 𝕜 s = ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • s
[PROOFSTEP]
refine' balancedCore_subset_balancedCoreAux.antisymm _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ balancedCoreAux 𝕜 s ⊆ balancedCore 𝕜 s
[PROOFSTEP]
refine' (balancedCoreAux_balanced _).subset_balancedCore_of_subset (balancedCoreAux_subset s)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : 0 ∈ s
⊢ 0 ∈ balancedCoreAux 𝕜 s
[PROOFSTEP]
exact balancedCore_subset_balancedCoreAux (balancedCore_zero_mem hs)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ balancedCore 𝕜 t
[PROOFSTEP]
rw [balancedCore_eq_iInter ht]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ ⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • t
[PROOFSTEP]
refine' subset_iInter₂ fun a ha => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • t
[PROOFSTEP]
rw [← smul_inv_smul₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha) s]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ a • a⁻¹ • s ⊆ a • t
[PROOFSTEP]
refine' smul_set_mono (hst _ _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1
[PROOFSTEP]
exact inv_le_one ha
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
⊢ IsClosed (balancedCore 𝕜 U)
[PROOFSTEP]
by_cases h : (0 : E) ∈ U
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
⊢ IsClosed (balancedCore 𝕜 U)
[PROOFSTEP]
rw [balancedCore_eq_iInter h]
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
⊢ IsClosed (⋂ (r : 𝕜) (_ : 1 ≤ ‖r‖), r • U)
[PROOFSTEP]
refine' isClosed_iInter fun a => _
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
⊢ IsClosed (⋂ (_ : 1 ≤ ‖a‖), a • U)
[PROOFSTEP]
refine' isClosed_iInter fun ha => _
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ IsClosed (a • U)
[PROOFSTEP]
have ha' := lt_of_lt_of_le zero_lt_one ha
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : 0 < ‖a‖
⊢ IsClosed (a • U)
[PROOFSTEP]
rw [norm_pos_iff] at ha'
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : 0 ∈ U
a : 𝕜
ha : 1 ≤ ‖a‖
ha' : a ≠ 0
⊢ IsClosed (a • U)
[PROOFSTEP]
exact isClosedMap_smul_of_ne_zero ha' U hU
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
⊢ IsClosed (balancedCore 𝕜 U)
[PROOFSTEP]
have : balancedCore 𝕜 U = ∅ := by
  contrapose! h
  exact balancedCore_nonempty_iff.mp (Set.nonempty_iff_ne_empty.2 h)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
⊢ balancedCore 𝕜 U = ∅
[PROOFSTEP]
contrapose! h
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : balancedCore 𝕜 U ≠ ∅
⊢ 0 ∈ U
[PROOFSTEP]
exact balancedCore_nonempty_iff.mp (Set.nonempty_iff_ne_empty.2 h)
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed (balancedCore 𝕜 U)
[PROOFSTEP]
rw [this]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : IsClosed U
h : ¬0 ∈ U
this : balancedCore 𝕜 U = ∅
⊢ IsClosed ∅
[PROOFSTEP]
exact isClosed_empty
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0
[PROOFSTEP]
obtain ⟨r, V, hr, hV, hrVU⟩ :
  ∃ (r : ℝ) (V : Set E), 0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U :=
  by
  have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
    continuous_smul.tendsto' (0, 0) _ (smul_zero _)
  simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
    h.basis_left (NormedAddCommGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
[PROOFSTEP]
have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
  continuous_smul.tendsto' (0, 0) _ (smul_zero _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
h : Tendsto (fun x => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0)
⊢ ∃ r V, 0 < r ∧ V ∈ 𝓝 0 ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
[PROOFSTEP]
simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
  h.basis_left (NormedAddCommGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
⊢ balancedCore 𝕜 U ∈ 𝓝 0
[PROOFSTEP]
rcases NormedField.exists_norm_lt 𝕜 hr with ⟨y, hy₀, hyr⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : 0 < ‖y‖
hyr : ‖y‖ < r
⊢ balancedCore 𝕜 U ∈ 𝓝 0
[PROOFSTEP]
rw [norm_pos_iff] at hy₀
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
⊢ balancedCore 𝕜 U ∈ 𝓝 0
[PROOFSTEP]
have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
this : y • V ∈ 𝓝 0
⊢ balancedCore 𝕜 U ∈ 𝓝 0
[PROOFSTEP]
refine' Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => _)
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • y • V ⊆ U
[PROOFSTEP]
rw [smul_smul]
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ (a * y) • V ⊆ U
[PROOFSTEP]
rintro _ ⟨z, hz, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ (fun x => (a * y) • x) z ∈ U
[PROOFSTEP]
refine' hrVU _ _ _ hz
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a * y‖ < r
[PROOFSTEP]
rw [norm_mul, ← one_mul r]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
U : Set E
hU : U ∈ 𝓝 0
r : ℝ
V : Set E
hr : 0 < r
hV : V ∈ 𝓝 0
hrVU : ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U
y : 𝕜
hy₀ : y ≠ 0
hyr : ‖y‖ < r
this : y • V ∈ 𝓝 0
a : 𝕜
ha : ‖a‖ ≤ 1
z : E
hz : z ∈ V
⊢ ‖a‖ * ‖y‖ < 1 * r
[PROOFSTEP]
exact mul_lt_mul' ha hyr (norm_nonneg y) one_pos
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : RegularSpace E
⊢ HasBasis (𝓝 0) (fun s => s ∈ 𝓝 0 ∧ IsClosed s ∧ Balanced 𝕜 s) id
[PROOFSTEP]
refine' (closed_nhds_basis 0).to_hasBasis (fun s hs => _) fun s hs => ⟨s, ⟨hs.1, hs.2.1⟩, rfl.subset⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ IsClosed i' ∧ Balanced 𝕜 i') ∧ id i' ⊆ id s
[PROOFSTEP]
refine' ⟨balancedCore 𝕜 s, ⟨balancedCore_mem_nhds_zero hs.1, _⟩, balancedCore_subset s⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕜 E
U : Set E
inst✝ : RegularSpace E
s : Set E
hs : s ∈ 𝓝 0 ∧ IsClosed s
⊢ IsClosed (balancedCore 𝕜 s) ∧ Balanced 𝕜 (balancedCore 𝕜 s)
[PROOFSTEP]
exact ⟨hs.2.balancedCore, balancedCore_balanced s⟩


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
⊢ Filter.HasBasis (𝓝 0) (fun s => s ∈ 𝓝 0 ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
[PROOFSTEP]
refine'
  (LocallyConvexSpace.convex_basis_zero ℝ E).to_hasBasis (fun s hs => _) fun s hs => ⟨s, ⟨hs.1, hs.2.2⟩, rfl.subset⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ∃ i', (i' ∈ 𝓝 0 ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
[PROOFSTEP]
refine' ⟨convexHull ℝ (balancedCore 𝕜 s), _, convexHull_min (balancedCore_subset s) hs.2⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ ↑(convexHull ℝ) (balancedCore 𝕜 s) ∈ 𝓝 0 ∧
    Balanced 𝕜 (↑(convexHull ℝ) (balancedCore 𝕜 s)) ∧ Convex ℝ (↑(convexHull ℝ) (balancedCore 𝕜 s))
[PROOFSTEP]
refine' ⟨Filter.mem_of_superset (balancedCore_mem_nhds_zero hs.1) (subset_convexHull ℝ _), _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Balanced 𝕜 (↑(convexHull ℝ) (balancedCore 𝕜 s)) ∧ Convex ℝ (↑(convexHull ℝ) (balancedCore 𝕜 s))
[PROOFSTEP]
refine' ⟨balanced_convexHull_of_balanced (balancedCore_balanced s), _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module ℝ E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : s ∈ 𝓝 0 ∧ Convex ℝ s
⊢ Convex ℝ (↑(convexHull ℝ) (balancedCore 𝕜 s))
[PROOFSTEP]
exact convex_convexHull ℝ (balancedCore 𝕜 s)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ Filter.HasBasis (𝓝 0) (fun s => 0 ∈ s ∧ IsOpen s ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
[PROOFSTEP]
refine' (nhds_basis_abs_convex 𝕜 E).to_hasBasis _ _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ ∀ (i : Set E),
    i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i → ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id i
[PROOFSTEP]
rintro s ⟨hs_nhds, hs_balanced, hs_convex⟩
[GOAL]
case refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_nhds : s ∈ 𝓝 0
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ ∃ i', (0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
[PROOFSTEP]
refine' ⟨interior s, _, interior_subset⟩
[GOAL]
case refine'_1.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_nhds : s ∈ 𝓝 0
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ 0 ∈ interior s ∧ IsOpen (interior s) ∧ Balanced 𝕜 (interior s) ∧ Convex ℝ (interior s)
[PROOFSTEP]
exact
  ⟨mem_interior_iff_mem_nhds.mpr hs_nhds, isOpen_interior, hs_balanced.interior (mem_interior_iff_mem_nhds.mpr hs_nhds),
    hs_convex.interior⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
⊢ ∀ (i' : Set E),
    0 ∈ i' ∧ IsOpen i' ∧ Balanced 𝕜 i' ∧ Convex ℝ i' → ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id i'
[PROOFSTEP]
rintro s ⟨hs_zero, hs_open, hs_balanced, hs_convex⟩
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
s✝ : Set E
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : LocallyConvexSpace ℝ E
inst✝² : ContinuousSMul 𝕜 E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : TopologicalAddGroup E
s : Set E
hs_zero : 0 ∈ s
hs_open : IsOpen s
hs_balanced : Balanced 𝕜 s
hs_convex : Convex ℝ s
⊢ ∃ i, (i ∈ 𝓝 0 ∧ Balanced 𝕜 i ∧ Convex ℝ i) ∧ id i ⊆ id s
[PROOFSTEP]
exact ⟨s, ⟨hs_open.mem_nhds hs_zero, hs_balanced, hs_convex⟩, rfl.subset⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Zero E
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul ℝ E
⊢ Nonempty (AbsConvexOpenSets 𝕜 E)
[PROOFSTEP]
rw [← exists_true_iff_nonempty]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Zero E
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul ℝ E
⊢ ∃ x, True
[PROOFSTEP]
dsimp only [AbsConvexOpenSets]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Zero E
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul ℝ E
⊢ ∃ x, True
[PROOFSTEP]
rw [Subtype.exists]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommMonoid E
inst✝³ : Zero E
inst✝² : SeminormedRing 𝕜
inst✝¹ : SMul 𝕜 E
inst✝ : SMul ℝ E
⊢ ∃ a b, True
[PROOFSTEP]
exact ⟨Set.univ, ⟨mem_univ 0, isOpen_univ, balanced_univ, convex_univ⟩, trivial⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ Seminorm.ball (gaugeSeminormFamily 𝕜 E s) 0 1 = ↑s
[PROOFSTEP]
dsimp only [gaugeSeminormFamily]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ Seminorm.ball (gaugeSeminorm (_ : Balanced 𝕜 ↑s) (_ : Convex ℝ ↑s) (_ : Absorbent ℝ ↑s)) 0 1 = ↑s
[PROOFSTEP]
rw [Seminorm.ball_zero_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | ↑(gaugeSeminorm (_ : Balanced 𝕜 ↑s) (_ : Convex ℝ ↑s) (_ : Absorbent ℝ ↑s)) y < 1} = ↑s
[PROOFSTEP]
simp_rw [gaugeSeminorm_toFun]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : Module ℝ E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousSMul ℝ E
s : AbsConvexOpenSets 𝕜 E
⊢ {y | gauge (↑s) y < 1} = ↑s
[PROOFSTEP]
exact gauge_lt_one_eq_self_of_open s.coe_convex s.coe_zero_mem s.coe_isOpen
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
refine' SeminormFamily.withSeminorms_of_hasBasis _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
refine' (nhds_basis_abs_convex_open 𝕜 E).to_hasBasis (fun s hs => _) fun s hs => _
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
refine' ⟨s, ⟨_, rfl.subset⟩⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
convert (gaugeSeminormFamily _ _).basisSets_singleton_mem ⟨s, hs⟩ one_pos
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
rw [gaugeSeminormFamily_ball, Subtype.coe_mk]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
refine' ⟨s, ⟨_, rfl.subset⟩⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
rw [SeminormFamily.basisSets_iff] at hs
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
rcases hs with ⟨t, r, hr, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
rw [Seminorm.ball_finset_sup_eq_iInter _ _ _ hr]
  -- We have to show that the intersection contains zero, is open, balanced, and convex
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
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 _ _ _⟩
    -- The only nontrivial part is to show that the ball is open
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
simp [Seminorm.mem_ball_zero, hr]
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
have hr' : r = ‖(r : 𝕜)‖ * 1 := by simp [abs_of_pos hr]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
simp [abs_of_pos hr]
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
have hr'' : (r : 𝕜) ≠ 0 := by simp [hr.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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
[PROOFSTEP]
simp [hr.ne']
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
rw [hr', ← Seminorm.smul_ball_zero hr'', gaugeSeminormFamily_ball]
[GOAL]
case refine'_2.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
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)
[PROOFSTEP]
exact S.coe_isOpen.smul₀ hr''