chore(analysis/locally_convex/basic): generalize lemmas and add simpl…

…e lemmas (#12643)

Gerenalize all 'simple' lemmas for `absorb` and `absorbent` to the type-class `[semi_normed_ring 𝕜] [has_scalar 𝕜 E]`.
Additionally, add the lemmas `absorbs_empty`, `balanced_mem` and `zero_singleton_balanced`.

src/analysis/locally_convex/basic.lean

@@ -49,40 +49,10 @@ variables (𝕜) [has_scalar 𝕜 E]
 sufficiently large norm. -/
 def absorbs (A B : set E) := ∃ r, 0 < r ∧ ∀ a : 𝕜, r ≤ ∥a∥ → B ⊆ a • A
 
-/-- A set is absorbent if it absorbs every singleton. -/
-def absorbent (A : set E) := ∀ x, ∃ r, 0 < r ∧ ∀ a : 𝕜, r ≤ ∥a∥ → x ∈ a • A
-
-/-- A set `A` is balanced if `a • A` is contained in `A` whenever `a` has norm at most `1`. -/
-def balanced (A : set E) := ∀ a : 𝕜, ∥a∥ ≤ 1 → a • A ⊆ A
-
-variables {𝕜} {A B : set E}
-
-lemma balanced_univ : balanced 𝕜 (univ : set E) := λ a ha, subset_univ _
-
-lemma balanced.union (hA : balanced 𝕜 A) (hB : balanced 𝕜 B) : balanced 𝕜 (A ∪ B) :=
-begin
-  intros a ha t ht,
-  rw smul_set_union at ht,
-  exact ht.imp (λ x, hA _ ha x) (λ x, hB _ ha x),
-end
-
-end has_scalar
+variables {𝕜} {s t u v A B : set E}
 
-section add_comm_group
-variables [add_comm_group E] [module 𝕜 E] {s t u v A B : set E}
-
-lemma balanced.inter (hA : balanced 𝕜 A) (hB : balanced 𝕜 B) : balanced 𝕜 (A ∩ B) :=
-begin
-  rintro a ha _ ⟨x, ⟨hx₁, hx₂⟩, rfl⟩,
-  exact ⟨hA _ ha ⟨_, hx₁, rfl⟩, hB _ ha ⟨_, hx₂, rfl⟩⟩,
-end
-
-lemma balanced.add (hA₁ : balanced 𝕜 A) (hA₂ : balanced 𝕜 B) : balanced 𝕜 (A + B) :=
-begin
-  rintro a ha _ ⟨_, ⟨x, y, hx, hy, rfl⟩, rfl⟩,
-  rw smul_add,
-  exact add_mem_add (hA₁ _ ha ⟨_, hx, rfl⟩) (hA₂ _ ha ⟨_, hy, rfl⟩),
-end
+lemma absorbs_empty {s : set E}: absorbs 𝕜 s (∅ : set E) :=
+⟨1, one_pos, λ a ha, set.empty_subset _⟩
 
 lemma absorbs.mono (hs : absorbs 𝕜 s u) (hst : s ⊆ t) (hvu : v ⊆ u) : absorbs 𝕜 t v :=
 let ⟨r, hr, h⟩ := hs in ⟨r, hr, λ a ha, hvu.trans $ (h _ ha).trans $ smul_set_mono hst⟩
@@ -102,6 +72,13 @@ end
 ⟨λ h, ⟨h.mono_right $ subset_union_left _ _, h.mono_right $ subset_union_right _ _⟩,
   λ h, h.1.union h.2⟩
 
+variables (𝕜)
+
+/-- A set is absorbent if it absorbs every singleton. -/
+def absorbent (A : set E) := ∀ x, ∃ r, 0 < r ∧ ∀ a : 𝕜, r ≤ ∥a∥ → x ∈ a • A
+
+variables {𝕜}
+
 lemma absorbent.subset (hA : absorbent 𝕜 A) (hAB : A ⊆ B) : absorbent 𝕜 B :=
 begin
   refine forall_imp (λ x, _) hA,
@@ -119,7 +96,48 @@ forall_congr $ λ x, ⟨λ ⟨r, hr, hx⟩, ⟨r, hr.le, λ a ha, hx a ha.le⟩,
   ⟨r + 1, add_pos_of_nonneg_of_pos hr zero_lt_one,
     λ a ha, hx ((lt_add_of_pos_right r zero_lt_one).trans_le ha)⟩⟩
 
-end add_comm_group
+variables (𝕜)
+
+/-- A set `A` is balanced if `a • A` is contained in `A` whenever `a` has norm at most `1`. -/
+def balanced (A : set E) := ∀ a : 𝕜, ∥a∥ ≤ 1 → a • A ⊆ A
+
+variables {𝕜}
+
+lemma balanced_mem {s : set E} (hs : balanced 𝕜 s) {x : E} (hx : x ∈ s) {a : 𝕜} (ha : ∥a∥ ≤ 1) :
+  a • x ∈ s :=
+mem_of_subset_of_mem (hs a ha) (smul_mem_smul_set hx)
+
+lemma balanced_univ : balanced 𝕜 (univ : set E) := λ a ha, subset_univ _
+
+lemma balanced.union (hA : balanced 𝕜 A) (hB : balanced 𝕜 B) : balanced 𝕜 (A ∪ B) :=
+begin
+  intros a ha t ht,
+  rw smul_set_union at ht,
+  exact ht.imp (λ x, hA _ ha x) (λ x, hB _ ha x),
+end
+
+lemma balanced.inter (hA : balanced 𝕜 A) (hB : balanced 𝕜 B) : balanced 𝕜 (A ∩ B) :=
+begin
+  rintro a ha _ ⟨x, ⟨hx₁, hx₂⟩, rfl⟩,
+  exact ⟨hA _ ha ⟨_, hx₁, rfl⟩, hB _ ha ⟨_, hx₂, rfl⟩⟩,
+end
+
+end has_scalar
+
+section add_comm_monoid
+variables [add_comm_monoid E] [module 𝕜 E] {s t u v A B : set E}
+
+lemma balanced.add (hA₁ : balanced 𝕜 A) (hA₂ : balanced 𝕜 B) : balanced 𝕜 (A + B) :=
+begin
+  rintro a ha _ ⟨_, ⟨x, y, hx, hy, rfl⟩, rfl⟩,
+  rw smul_add,
+  exact add_mem_add (hA₁ _ ha ⟨_, hx, rfl⟩) (hA₂ _ ha ⟨_, hy, rfl⟩),
+end
+
+lemma zero_singleton_balanced : balanced 𝕜 ({0} : set E) :=
+λ a ha, by simp only [smul_set_singleton, smul_zero]
+
+end add_comm_monoid
 end semi_normed_ring
 
 section normed_comm_ring