Update Separation.lean

Author: CoolRmal

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -324,8 +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. This is Lemma 1.2.9 in
-[Hytonen_VanNeerven_Veraar_Wies_2016]. -/
+space. Moreover, these halfspaces are all nontrivial if `s` is nonempty. -/
 theorem iInter_nat_halfSpaces_eq
     (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) (hsep : IsSeparable sᶜ) :
     ∃ (L : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),