[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hu : Absorbs 𝕜 s u
hv : Absorbs 𝕜 s v
⊢ Absorbs 𝕜 s (u ∪ v)
[PROOFSTEP]
obtain ⟨a, ha, hu⟩ := hu
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hv : Absorbs 𝕜 s v
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 s (u ∪ v)
[PROOFSTEP]
obtain ⟨b, _hb, hv⟩ := hv
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
a : ℝ
ha : 0 < a
hu : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
hv : ∀ (a : 𝕜), b ≤ ‖a‖ → v ⊆ a • s
⊢ Absorbs 𝕜 s (u ∪ v)
[PROOFSTEP]
exact
  ⟨max a b, lt_max_of_lt_left ha, fun c hc =>
    union_subset (hu _ <| le_of_max_le_left hc) (hv _ <| le_of_max_le_right hc)⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
t : Finset ι
f : ι → Set E
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
classical
induction' t using Finset.induction_on with i t _ht hi
· simp only [Finset.not_mem_empty, Set.iUnion_false, Set.iUnion_empty, absorbs_empty, IsEmpty.forall_iff, imp_true_iff]
rw [Finset.set_biUnion_insert, absorbs_union, hi]
constructor <;> intro h
· refine' fun _ hi' => (Finset.mem_insert.mp hi').elim _ (h.2 _)
  exact fun hi'' => by
    rw [hi'']
    exact h.1
exact ⟨h i (Finset.mem_insert_self i t), fun i' hi' => h i' (Finset.mem_insert_of_mem hi')⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
t : Finset ι
f : ι → Set E
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
induction' t using Finset.induction_on with i t _ht hi
[GOAL]
case empty
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
ι : Type u_6
f : ι → Set E
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ ∅), f i) ↔ ∀ (i : ι), i ∈ ∅ → Absorbs 𝕜 s (f i)
[PROOFSTEP]
simp only [Finset.not_mem_empty, Set.iUnion_false, Set.iUnion_empty, absorbs_empty, IsEmpty.forall_iff, imp_true_iff]
[GOAL]
case insert
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ Absorbs 𝕜 s (⋃ (i_1 : ι) (_ : i_1 ∈ insert i t), f i_1) ↔ ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
rw [Finset.set_biUnion_insert, absorbs_union, hi]
[GOAL]
case insert
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ (Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)) ↔ ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
constructor
[GOAL]
case insert.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ (Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)) → ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
intro h
[GOAL]
case insert.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ (∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)) → Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
intro h
[GOAL]
case insert.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
⊢ ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
[PROOFSTEP]
refine' fun _ hi' => (Finset.mem_insert.mp hi').elim _ (h.2 _)
[GOAL]
case insert.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
x✝ : ι
hi' : x✝ ∈ insert i t
⊢ x✝ = i → Absorbs 𝕜 s (f x✝)
[PROOFSTEP]
exact fun hi'' => by
  rw [hi'']
  exact h.1
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
x✝ : ι
hi' : x✝ ∈ insert i t
hi'' : x✝ = i
⊢ Absorbs 𝕜 s (f x✝)
[PROOFSTEP]
rw [hi'']
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
x✝ : ι
hi' : x✝ ∈ insert i t
hi'' : x✝ = i
⊢ Absorbs 𝕜 s (f i)
[PROOFSTEP]
exact h.1
[GOAL]
case insert.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t✝ u v A B : Set E
ι : Type u_6
f : ι → Set E
i : ι
t : Finset ι
_ht : ¬i ∈ t
hi : Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
h : ∀ (i_1 : ι), i_1 ∈ insert i t → Absorbs 𝕜 s (f i_1)
⊢ Absorbs 𝕜 s (f i) ∧ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
exact ⟨h i (Finset.mem_insert_self i t), fun i' hi' => h i' (Finset.mem_insert_of_mem hi')⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_6
s : Set E
t : Set ι
f : ι → Set E
hi : Set.Finite t
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
lift t to Finset ι using hi
[GOAL]
case intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_6
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ ↑t), f i) ↔ ∀ (i : ι), i ∈ ↑t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
simp only [Finset.mem_coe]
[GOAL]
case intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι✝ : Sort u_4
κ : ι✝ → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t✝ u v A B : Set E
ι : Type u_6
s : Set E
f : ι → Set E
t : Finset ι
⊢ Absorbs 𝕜 s (⋃ (i : ι) (_ : i ∈ t), f i) ↔ ∀ (i : ι), i ∈ t → Absorbs 𝕜 s (f i)
[PROOFSTEP]
exact absorbs_iUnion_finset
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
⊢ Absorbent 𝕜 B
[PROOFSTEP]
refine' forall_imp (fun x => _) hA
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
hA : Absorbent 𝕜 A
hAB : A ⊆ B
x : E
⊢ (∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A) → ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • B
[PROOFSTEP]
exact Exists.imp fun r => And.imp_right <| forall₂_imp fun a _ha hx => Set.smul_set_mono hAB hx
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
⊢ Absorbent 𝕜 A ↔ ∀ (x : E), Absorbs 𝕜 A {x}
[PROOFSTEP]
simp_rw [Absorbs, Absorbent, singleton_subset_iff]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s v
[PROOFSTEP]
rw [← Set.biUnion_of_singleton v]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s✝ t u v✝ A B s : Set E
hs : Absorbent 𝕜 s
v : Set E
hv : Set.Finite v
⊢ Absorbs 𝕜 s (⋃ (x : E) (_ : x ∈ v), {x})
[PROOFSTEP]
exact hv.absorbs_iUnion.mpr fun _ _ => hs.absorbs
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t u v A B : Set E
x✝¹ : 𝕜
x✝ : ‖x✝¹‖ ≤ 1
⊢ x✝¹ • ∅ ⊆ ∅
[PROOFSTEP]
rw [smul_set_empty]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ - s₂) (t₁ - t₂)
[PROOFSTEP]
simp_rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
h₁ : Absorbs 𝕜 s₁ t₁
h₂ : Absorbs 𝕜 s₂ t₂
⊢ Absorbs 𝕜 (s₁ + -s₂) (t₁ + -t₂)
[PROOFSTEP]
exact h₁.add h₂.neg
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s - t)
[PROOFSTEP]
simp_rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s s₁ s₂ t t₁ t₂ : Set E
hs : Balanced 𝕜 s
ht : Balanced 𝕜 t
⊢ Balanced 𝕜 (s + -t)
[PROOFSTEP]
exact hs.add ht.neg
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
⊢ a • s ⊆ b • s
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ ‖0‖
⊢ a • s ⊆ 0 • s
[PROOFSTEP]
rw [norm_zero] at h 
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ a • s ⊆ 0 • s
[PROOFSTEP]
rw [norm_eq_zero.1 (h.antisymm <| norm_nonneg _)]
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h : ‖a‖ ≤ 0
⊢ 0 • s ⊆ 0 • s
[PROOFSTEP]
obtain rfl | h := s.eq_empty_or_nonempty
[GOAL]
case inl.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ 0 • ∅ ⊆ 0 • ∅
[PROOFSTEP]
simp_rw [smul_set_empty]
[GOAL]
case inl.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
t u v A B : Set E
x : E
a✝ b : 𝕜
a : 𝕝
h : ‖a‖ ≤ 0
hs : Balanced 𝕝 ∅
⊢ ∅ ⊆ ∅
[PROOFSTEP]
rfl
[GOAL]
case inl.inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 • s ⊆ 0 • s
[PROOFSTEP]
simp_rw [zero_smul_set h]
[GOAL]
case inl.inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
h✝ : ‖a‖ ≤ 0
h : Set.Nonempty s
⊢ 0 ⊆ 0
[PROOFSTEP]
rfl
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
⊢ a • s ⊆ b • s
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (fun x => a • x) x ∈ b • s
[PROOFSTEP]
refine' ⟨b⁻¹ • a • x, _, smul_inv_smul₀ hb _⟩
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ b⁻¹ • a • x ∈ s
[PROOFSTEP]
rw [← smul_assoc]
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ (b⁻¹ • a) • x ∈ s
[PROOFSTEP]
refine' hs _ _ (smul_mem_smul_set hx)
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖b⁻¹ • a‖ ≤ 1
[PROOFSTEP]
rw [norm_smul, norm_inv, ← div_eq_inv_mul]
[GOAL]
case inr.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b✝ : 𝕜
hs : Balanced 𝕝 s
a : 𝕝
b : 𝕜
h : ‖a‖ ≤ ‖b‖
hb : b ≠ 0
x : E
hx : x ∈ s
⊢ ‖a‖ / ‖b‖ ≤ 1
[PROOFSTEP]
exact div_le_one_of_le h (norm_nonneg _)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
⊢ Absorbs 𝕜 A A
[PROOFSTEP]
refine' ⟨1, zero_lt_one, fun a ha x hx => _⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ x ∈ a • A
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.1 <| zero_lt_one.trans_le ha)]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ a⁻¹ • x ∈ A
[PROOFSTEP]
refine' hA a⁻¹ _ (smul_mem_smul_set hx)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
hA : Balanced 𝕜 A
a : 𝕜
ha : 1 ≤ ‖a‖
x : E
hx : x ∈ A
⊢ ‖a‖⁻¹ ≤ 1
[PROOFSTEP]
exact inv_le_one ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ A ⊆ a • A
[PROOFSTEP]
refine' (subset_set_smul_iff₀ _).2 (hA a⁻¹ _)
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖0‖
⊢ False
[PROOFSTEP]
rw [norm_zero] at ha 
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ 0
⊢ False
[PROOFSTEP]
exact zero_lt_one.not_le ha
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1
[PROOFSTEP]
rw [norm_inv]
[GOAL]
case refine'_2
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hA : Balanced 𝕜 A
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1
[PROOFSTEP]
exact inv_le_one ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
obtain rfl | hb := eq_or_ne b 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖0‖
⊢ a • x ∈ s ↔ 0 • x ∈ s
[PROOFSTEP]
rw [norm_zero, norm_eq_zero] at h 
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a : 𝕜
hs : Balanced 𝕜 s
h : a = 0
⊢ a • x ∈ s ↔ 0 • x ∈ s
[PROOFSTEP]
rw [h]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
have ha : a ≠ 0 := norm_ne_zero_iff.1 (ne_of_eq_of_ne h <| norm_ne_zero_iff.2 hb)
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
constructor <;> intro h' <;> [rw [← inv_mul_cancel_right₀ ha b]; rw [← inv_mul_cancel_right₀ hb a]]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s ↔ b • x ∈ s
[PROOFSTEP]
constructor
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ a • x ∈ s → b • x ∈ s
[PROOFSTEP]
intro h'
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
⊢ b • x ∈ s → a • x ∈ s
[PROOFSTEP]
intro h'
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ b • x ∈ s
[PROOFSTEP]
rw [← inv_mul_cancel_right₀ ha b]
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ a • x ∈ s
[PROOFSTEP]
rw [← inv_mul_cancel_right₀ hb a]
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ (b * a⁻¹ * a) • x ∈ s
[PROOFSTEP]
rw [← smul_eq_mul, smul_assoc]
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ (b * a⁻¹) • a • x ∈ s
[PROOFSTEP]
refine' hs.smul_mem _ h'
[GOAL]
case inr.mp
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : a • x ∈ s
⊢ ‖b * a⁻¹‖ ≤ 1
[PROOFSTEP]
simp [← h, ha]
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹ * b) • x ∈ s
[PROOFSTEP]
rw [← smul_eq_mul, smul_assoc]
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ (a * b⁻¹) • b • x ∈ s
[PROOFSTEP]
refine' hs.smul_mem _ h'
[GOAL]
case inr.mpr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
h : ‖a‖ = ‖b‖
hb : b ≠ 0
ha : a ≠ 0
h' : b • x ∈ s
⊢ ‖a * b⁻¹‖ ≤ 1
[PROOFSTEP]
simp [← h, ha]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ -x ∈ s ↔ x ∈ s
[PROOFSTEP]
convert hs.mem_smul_iff (x := x) (norm_neg 1) using 0
[GOAL]
case a
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Balanced 𝕜 s
⊢ (-x ∈ s ↔ x ∈ s) ↔ (-1 • x ∈ s ↔ 1 • x ∈ s)
[PROOFSTEP]
simp only [neg_smul, one_smul 𝕜 x]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
hs : Absorbs 𝕜 s u
ht : Absorbs 𝕜 t u
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
obtain ⟨a, ha, hs⟩ := hs
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
ht : Absorbs 𝕜 t u
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
obtain ⟨b, _hb, ht⟩ := ht
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
have h : 0 < max a b := lt_max_of_lt_left ha
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
⊢ Absorbs 𝕜 (s ∩ t) u
[PROOFSTEP]
refine' ⟨max a b, lt_max_of_lt_left ha, fun c hc => _⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • (s ∩ t)
[PROOFSTEP]
rw [smul_set_inter₀ (norm_pos_iff.1 <| h.trans_le hc)]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b✝ : 𝕜
a : ℝ
ha : 0 < a
hs : ∀ (a_1 : 𝕜), a ≤ ‖a_1‖ → u ⊆ a_1 • s
b : ℝ
_hb : 0 < b
ht : ∀ (a : 𝕜), b ≤ ‖a‖ → u ⊆ a • t
h : 0 < max a b
c : 𝕜
hc : max a b ≤ ‖c‖
⊢ u ⊆ c • s ∩ c • t
[PROOFSTEP]
exact subset_inter (hs _ <| le_of_max_le_left hc) (ht _ <| le_of_max_le_right hc)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
⊢ Absorbent 𝕜 univ
[PROOFSTEP]
refine' fun x => ⟨1, zero_lt_one, fun a ha => _⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ a • univ
[PROOFSTEP]
rw [smul_set_univ₀ (norm_pos_iff.1 <| zero_lt_one.trans_le ha)]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedRing 𝕝
inst✝⁴ : NormedSpace 𝕜 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : SMulWithZero 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
x : E
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ x ∈ univ
[PROOFSTEP]
exact trivial
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
⊢ Absorbent 𝕜 A
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
obtain ⟨w, hw₁, hw₂, hw₃⟩ := mem_nhds_iff.mp hA
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
have hc : Continuous fun t : 𝕜 => t • x := continuous_id.smul continuous_const
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
obtain ⟨r, hr₁, hr₂⟩ := Metric.isOpen_iff.mp (hw₂.preimage hc) 0 (by rwa [mem_preimage, zero_smul])
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
⊢ 0 ∈ (fun t => t • x) ⁻¹' w
[PROOFSTEP]
rwa [mem_preimage, zero_smul]
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
have hr₃ := inv_pos.mpr (half_pos hr₁)
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
⊢ ∃ r, 0 < r ∧ ∀ (a : 𝕜), r ≤ ‖a‖ → x ∈ a • A
[PROOFSTEP]
refine' ⟨(r / 2)⁻¹, hr₃, fun a ha₁ => _⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
⊢ x ∈ a • A
[PROOFSTEP]
have ha₂ : 0 < ‖a‖ := hr₃.trans_le ha₁
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
ha₂ : 0 < ‖a‖
⊢ x ∈ a • A
[PROOFSTEP]
refine' (mem_smul_set_iff_inv_smul_mem₀ (norm_pos_iff.mp ha₂) _ _).2 (hw₁ <| hr₂ _)
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
ha₂ : 0 < ‖a‖
⊢ a⁻¹ ∈ Metric.ball 0 r
[PROOFSTEP]
rw [Metric.mem_ball, dist_zero_right, norm_inv]
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x✝ : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : A ∈ 𝓝 0
x : E
w : Set E
hw₁ : w ⊆ A
hw₂ : IsOpen w
hw₃ : 0 ∈ w
hc : Continuous fun t => t • x
r : ℝ
hr₁ : r > 0
hr₂ : Metric.ball 0 r ⊆ (fun t => t • x) ⁻¹' w
hr₃ : 0 < (r / 2)⁻¹
a : 𝕜
ha₁ : (r / 2)⁻¹ ≤ ‖a‖
ha₂ : 0 < ‖a‖
⊢ ‖a‖⁻¹ < r
[PROOFSTEP]
calc
  ‖a‖⁻¹ ≤ r / 2 := (inv_le (half_pos hr₁) ha₂).mp ha₁
  _ < r := half_lt_self hr₁
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
⊢ Balanced 𝕜 (0 ∪ interior A)
[PROOFSTEP]
intro a ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • (0 ∪ interior A) ⊆ 0 ∪ interior A
[PROOFSTEP]
obtain rfl | h := eq_or_ne a 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ 0 • (0 ∪ interior A) ⊆ 0 ∪ interior A
[PROOFSTEP]
rw [zero_smul_set]
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ 0 ⊆ 0 ∪ interior A
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
ha : ‖0‖ ≤ 1
⊢ Set.Nonempty (0 ∪ interior A)
[PROOFSTEP]
exacts [subset_union_left _ _, ⟨0, Or.inl rfl⟩]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ a • (0 ∪ interior A) ⊆ 0 ∪ interior A
[PROOFSTEP]
rw [← image_smul, image_union]
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x => a • x) '' 0 ∪ (fun x => a • x) '' interior A ⊆ 0 ∪ interior A
[PROOFSTEP]
apply union_subset_union
[GOAL]
case inr.h₁
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x => a • x) '' 0 ⊆ 0
[PROOFSTEP]
rw [image_zero, smul_zero]
[GOAL]
case inr.h₁
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ {0} ⊆ 0
[PROOFSTEP]
rfl
[GOAL]
case inr.h₂
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a✝ b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
a : 𝕜
ha : ‖a‖ ≤ 1
h : a ≠ 0
⊢ (fun x => a • x) '' interior A ⊆ interior A
[PROOFSTEP]
calc
  a • interior A ⊆ interior (a • A) := (isOpenMap_smul₀ h).image_interior_subset A
  _ ⊆ interior A := interior_mono (hA _ ha)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 (_root_.interior A)
[PROOFSTEP]
rw [← union_eq_self_of_subset_left (singleton_subset_iff.2 h)]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕝
inst✝⁶ : NormedSpace 𝕜 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : SMulWithZero 𝕝 E
inst✝² : IsScalarTower 𝕜 𝕝 E
s t u v A B : Set E
x : E
a b : 𝕜
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul 𝕜 E
hA : Balanced 𝕜 A
h : 0 ∈ _root_.interior A
⊢ Balanced 𝕜 ({0} ∪ _root_.interior A)
[PROOFSTEP]
exact balanced_zero_union_interior hA
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 ↔ 0 ∈ s
[PROOFSTEP]
refine' ⟨_, fun h => ⟨1, zero_lt_one, fun a _ => zero_subset.2 <| zero_mem_smul_set h⟩⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ Absorbs 𝕜 s 0 → 0 ∈ s
[PROOFSTEP]
rintro ⟨r, hr, h⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
⊢ 0 ∈ s
[PROOFSTEP]
obtain ⟨a, ha⟩ := NormedSpace.exists_lt_norm 𝕜 𝕜 r
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
⊢ 0 ∈ s
[PROOFSTEP]
have := h _ ha.le
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ⊆ a • s
⊢ 0 ∈ s
[PROOFSTEP]
rwa [zero_subset, zero_mem_smul_set_iff] at this 
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
r : ℝ
hr : 0 < r
h : ∀ (a : 𝕜), r ≤ ‖a‖ → 0 ⊆ a • s
a : 𝕜
ha : r < ‖a‖
this : 0 ∈ a • s
⊢ a ≠ 0
[PROOFSTEP]
exact norm_ne_zero_iff.1 (hr.trans ha).ne'
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
⊢ Balanced 𝕜 (↑(convexHull ℝ) s)
[PROOFSTEP]
suffices Convex ℝ {x | ∀ a : 𝕜, ‖a‖ ≤ 1 → a • x ∈ convexHull ℝ s}
  by
  rw [balanced_iff_smul_mem] at hs ⊢
  refine' fun a ha x hx => convexHull_min _ this hx a ha
  exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
this : Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
⊢ Balanced 𝕜 (↑(convexHull ℝ) s)
[PROOFSTEP]
rw [balanced_iff_smul_mem] at hs ⊢
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
⊢ ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ ↑(convexHull ℝ) s → a • x ∈ ↑(convexHull ℝ) s
[PROOFSTEP]
refine' fun a ha x hx => convexHull_min _ this hx a ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : ∀ ⦃a : 𝕜⦄, ‖a‖ ≤ 1 → ∀ ⦃x : E⦄, x ∈ s → a • x ∈ s
this : Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
a : 𝕜
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ ↑(convexHull ℝ) s
⊢ s ⊆ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
[PROOFSTEP]
exact fun y hy a ha => subset_convexHull ℝ s (hs ha hy)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
⊢ Convex ℝ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
[PROOFSTEP]
intro x hx y hy u v hu hv huv a ha
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
u v : ℝ
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ a • (u • x + v • y) ∈ ↑(convexHull ℝ) s
[PROOFSTEP]
simp only [smul_add, ← smul_comm]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
s : Set E
inst✝¹ : Module ℝ E
inst✝ : SMulCommClass ℝ 𝕜 E
hs : Balanced 𝕜 s
x : E
hx : x ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
y : E
hy : y ∈ {x | ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • x ∈ ↑(convexHull ℝ) s}
u v : ℝ
hu : 0 ≤ u
hv : 0 ≤ v
huv : u + v = 1
a : 𝕜
ha : ‖a‖ ≤ 1
⊢ u • a • x + v • a • y ∈ ↑(convexHull ℝ) s
[PROOFSTEP]
exact convex_convexHull ℝ s (hx a ha) (hy a ha) hu hv huv
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
⊢ Balanced ℝ s ↔ ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
[PROOFSTEP]
refine' ⟨fun h x => h.neg_mem_iff.2, fun h a ha => smul_set_subset_iff.2 fun x hx => _⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : ‖a‖ ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
[PROOFSTEP]
rw [Real.norm_eq_abs, abs_le] at ha 
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a • x ∈ s
[PROOFSTEP]
rw [show a = -((1 - a) / 2) + (a - -1) / 2 by ring, add_smul, neg_smul, ← smul_neg]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ a = -((1 - a) / 2) + (a - -1) / 2
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ ((1 - a) / 2) • -x + ((a - -1) / 2) • x ∈ s
[PROOFSTEP]
exact
  hs (h hx) hx (div_nonneg (sub_nonneg_of_le ha.2) zero_le_two) (div_nonneg (sub_nonneg_of_le ha.1) zero_le_two)
    (by ring)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h : ∀ ⦃x : E⦄, x ∈ s → -x ∈ s
a : ℝ
ha : -1 ≤ a ∧ a ≤ 1
x : E
hx : x ∈ s
⊢ (1 - a) / 2 + (a - -1) / 2 = 1
[PROOFSTEP]
ring
