feat: port Topology.MetricSpace.Gluing (#2711)

Mathlib.lean

@@ -1415,6 +1415,7 @@ import Mathlib.Topology.MetricSpace.Completion
 import Mathlib.Topology.MetricSpace.EMetricParacompact
 import Mathlib.Topology.MetricSpace.EMetricSpace
 import Mathlib.Topology.MetricSpace.Equicontinuity
+import Mathlib.Topology.MetricSpace.Gluing
 import Mathlib.Topology.MetricSpace.Infsep
 import Mathlib.Topology.MetricSpace.IsometricSMul
 import Mathlib.Topology.MetricSpace.Isometry

Mathlib/Data/Real/Basic.lean

@@ -876,6 +876,12 @@ theorem infₛ_nonneg (S : Set ℝ) (hS : ∀ x ∈ S, (0 : ℝ) ≤ x) : 0 ≤
   exacts[infₛ_empty.ge, le_cinfₛ hS₂ hS]
 #align real.Inf_nonneg Real.infₛ_nonneg
 
+/-- As `0` is the default value for `Real.infₛ` of the empty set, it suffices to show that `f i` is
+bounded below by `0` to show that `0 ≤ infᵢ f`.
+-/
+theorem infᵢ_nonneg {ι} {f : ι → ℝ} (hf : ∀ i, 0 ≤ f i) : 0 ≤ infᵢ f :=
+  infₛ_nonneg _ <| Set.forall_range_iff.2 hf
+
 /--
 As `0` is the default value for `Real.infₛ` of the empty set or sets which are not bounded below, it
 suffices to show that `S` is bounded above by `0` to show that `infₛ S ≤ 0`.