fixed notation port to lip section in lp

leanprover-community · Jun 16, 2023 · 2a52137 · tb65536 · Jun 16, 2023 · 2a52137
1 parent f91fae3
commit 2a52137
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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