feat(Analysis/Convex/Basic): two useful lemmas on pointwise operations (leanprover-community#38598)

In proofs about locally convex spaces, it's common to need that `(1/2) * s + (1/2) * s = s` for convex `s` and that `closure s <= s + s` when `s` is open and contains `0`. We add these lemmas, which will be used ultimately in a proof of Michael's selection theorem.

Co-authored-by: Kevin H Wilson <khwilson@gmail.com>

Author: khwilson

Mathlib/Analysis/Convex/Basic.lean

@@ -570,6 +570,11 @@ protected theorem Convex.add_smul (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0
   rintro _ ⟨_, ⟨v₁, h₁, rfl⟩, _, ⟨v₂, h₂, rfl⟩, rfl⟩
   exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq
 
+theorem Convex.add_half_self_eq_self (h_conv : Convex 𝕜 s) : (2 : 𝕜)⁻¹ • s + (2 : 𝕜)⁻¹ • s = s := by
+  rw [← h_conv.add_smul (by norm_num) (by norm_num)]
+  ring_nf
+  rw [one_smul]
+
 end AddCommGroup
 
 end LinearOrderedField

Mathlib/Topology/Algebra/Group/Pointwise.lean

@@ -30,7 +30,6 @@ with continuous addition/multiplication. See also `Submonoid.top_closure_mul_sel
 `Topology.Algebra.Monoid`.
 -/
 
-
 section ContinuousConstSMul
 
 variable [TopologicalSpace β] [Group α] [MulAction α β] [ContinuousConstSMul α β] {s : Set α}
@@ -253,6 +252,16 @@ lemma IsOpen.mul_closure_one_eq {U : Set G} (hU : IsOpen U) :
     U * (closure {1} : Set G) = U :=
   compl_mul_closure_one_eq_iff.1 (hU.isClosed_compl.mul_closure_one_eq)
 
+@[to_additive]
+theorem closure_subset_mul_self_of_mem_nhds_one {U : Set G} (hU : U ∈ 𝓝 1) :
+    closure U ⊆ U * U := by
+  intro x hx
+  rw [mem_closure_iff_nhds] at hx
+  have hkey : (fun y => x / y) ⁻¹' U ∈ 𝓝 x :=
+    ContinuousAt.preimage_mem_nhds (by fun_prop) (by simpa)
+  obtain ⟨a, ha_mem, ha_s⟩ := hx _ hkey
+  exact Set.mem_mul.mpr ⟨x / a, ha_mem, a, ha_s, div_mul_cancel x a⟩
+
 end IsTopologicalGroup
 
 section FilterMul