fix typo

fpvandoorn · Jul 30, 2024 · b635481 · b635481
1 parent 5c259fc
commit b635481
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean
@@ -1468,7 +1468,7 @@ lemma L0_has_bounded_series (p : LTSeries (𝔏₀ (X := X) k n)) : p.length ≤
 lemma iUnion_L0' : ⋃ (l ≤ n), 𝔏₀' (X := X) k n l = 𝔏₀ k n :=
   Set.iUnion_withHeight_iff_bounded_series.mpr L0_has_bounded_series
 
-/-- Part of Lemma 5.5.2 -/repo, 
+/-- Part of Lemma 5.5.2 -/
 lemma pairwiseDisjoint_L0' : univ.PairwiseDisjoint (𝔏₀' (X := X) k n) :=
   Set.PairwiseDisjoint_withHeight _