Update Separation.lean

Author: CoolRmal

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -324,7 +324,7 @@ section Countable
 variable [NormedAddCommGroup E] [NormedSpace ℝ E] [Module 𝕜 E] [ContinuousSMul 𝕜 E]
 
 /-- A closed convex set `s` is the intersection of countably many half spaces in a separable Banach
-space. Moreover, these halfspaces are all nontrivial if `s` is nonempty. -/
+space. Moreover, these halfspaces are all nontrivial if `s` is nonempty and not equal to `univ`. -/
 theorem iInter_nat_halfSpaces_eq
     (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) (hsep : IsSeparable sᶜ) :
     ∃ (L : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),