feat: missing basic analysis and topology API (leanprover-community#34411)

Basic lemmas cherry picked from leanprover-community#34055.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -419,7 +419,7 @@ abbrev GroupNorm.toNormedCommGroup [CommGroup E] (f : GroupNorm E) : NormedCommG
 section SeminormedGroup
 
 variable [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {s : Set E}
-  {a a₁ a₂ b c : E} {r r₁ r₂ : ℝ}
+  {a a₁ a₂ b c d : E} {r r₁ r₂ : ℝ}
 
 @[to_additive]
 theorem dist_eq_norm_div (a b : E) : dist a b = ‖a / b‖ :=
@@ -495,6 +495,11 @@ theorem norm_mul_le_of_le' (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r
 @[to_additive norm_add₃_le /-- **Triangle inequality** for the norm. -/]
 lemma norm_mul₃_le' : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ := norm_mul_le_of_le' (norm_mul_le' _ _) le_rfl
 
+/-- **Triangle inequality** for the norm. -/
+@[to_additive norm_add₄_le /-- **Triangle inequality** for the norm. -/]
+lemma norm_mul₄_le' : ‖a * b * c * d‖ ≤ ‖a‖ + ‖b‖ + ‖c‖ + ‖d‖ :=
+  norm_mul_le_of_le' norm_mul₃_le' le_rfl
+
 @[to_additive]
 lemma norm_div_le_norm_div_add_norm_div (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖ := by
   simpa only [dist_eq_norm_div] using dist_triangle a b c
@@ -979,6 +984,19 @@ variable {E : Type*} [TopologicalSpace E] [ESeminormedMonoid E]
 @[to_additive enorm_add_le]
 lemma enorm_mul_le' (a b : E) : ‖a * b‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ := ESeminormedMonoid.enorm_mul_le a b
 
+@[to_additive enorm_add_le_of_le]
+theorem enorm_mul_le_of_le' {r₁ r₂ : ℝ≥0∞} {a₁ a₂ : E}
+    (h₁ : ‖a₁‖ₑ ≤ r₁) (h₂ : ‖a₂‖ₑ ≤ r₂) : ‖a₁ * a₂‖ₑ ≤ r₁ + r₂ :=
+  (enorm_mul_le' a₁ a₂).trans <| add_le_add h₁ h₂
+
+@[to_additive enorm_add₃_le]
+lemma enorm_mul₃_le' {a b c : E} : ‖a * b * c‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ :=
+  enorm_mul_le_of_le' (enorm_mul_le' _ _) le_rfl
+
+@[to_additive enorm_add₄_le]
+lemma enorm_mul₄_le' {a b c d : E} : ‖a * b * c * d‖ₑ ≤ ‖a‖ₑ + ‖b‖ₑ + ‖c‖ₑ + ‖d‖ₑ :=
+  enorm_mul_le_of_le' enorm_mul₃_le' le_rfl
+
 end ESeminormedMonoid
 
 section ENormedMonoid

Mathlib/Topology/ClusterPt.lean

@@ -174,6 +174,10 @@ theorem MapClusterPt.of_comp {φ : β → α} {p : Filter β} (h : Tendsto φ p
     (H : MapClusterPt x p (u ∘ φ)) : MapClusterPt x F u :=
   H.clusterPt.mono <| map_mono h
 
+theorem IsClosed.mem_of_mapClusterPt {l : X} {s : Set X} {f : α → X} {b : Filter α}
+    (hs : IsClosed s) (hf : MapClusterPt l b f) (h : ∀ᶠ (x : α) in b, f x ∈ s) : l ∈ s :=
+  (hf.frequently' h).mem_of_closed hs
+
 end MapClusterPt
 
 theorem accPt_sup {x : X} {F G : Filter X} :

Mathlib/Topology/NhdsWithin.lean

@@ -211,6 +211,10 @@ theorem nhds_eq_nhdsWithin_sup_nhdsWithin (b : α) {I₁ I₂ : Set α} (hI : Se
     nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂ := by
   rw [← nhdsWithin_univ b, hI, nhdsWithin_union]
 
+lemma inter_mem_nhdsWithin_inter {a b c d : Set α} {x : α} (h : a ∈ 𝓝[b] x) (h' : c ∈ 𝓝[d] x) :
+    a ∩ c ∈ 𝓝[b ∩ d] x :=
+  inter_mem (nhdsWithin_mono _ inter_subset_left h) (nhdsWithin_mono _ inter_subset_right h')
+
 /-- If `L` and `R` are neighborhoods of `b` within sets whose union is `Set.univ`, then
 `L ∪ R` is a neighborhood of `b`. -/
 theorem union_mem_nhds_of_mem_nhdsWithin {b : α}