From 2a521378c509a8fe2b7e3377ffb23a1b3755820b Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Fri, 16 Jun 2023 15:47:55 -0700
Subject: [PATCH] fixed notation port to lip section in lp

---
 Mathlib/Analysis/NormedSpace/lpSpace.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 79d8fca64a641..1fda5bfcb63b1 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -1223,6 +1223,10 @@ end lp
 
 section Lipschitz
 
+local notation "ℓ^∞(" ι ")" => lp (fun i : ι => ℝ) ∞
+
+open ENNReal
+
 lemma LipschitzWith.uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0}
     (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α) (hga₀b : Memℓp (g a₀) ∞) (a : α) :
     Memℓp (g a) ∞ := by