More PR references

fpvandoorn · Jul 30, 2024 · 9d3a124 · 9d3a124
1 parent da9eefb
commit 9d3a124
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Carleson/ToMathlib/Height.lean b/Carleson/ToMathlib/Height.lean
@@ -48,6 +48,7 @@ theorem ENat.lt_add_one_iff (n m : ℕ∞) (hm : n ≠ ⊤) : m < n + 1 ↔ m
   · norm_num
   · norm_cast; omega
 
+-- Parts of it in https://github.com/leanprover-community/mathlib4/pull/15347
 lemma ENat.iSup_eq_coe_iff' {α : Type*} [Nonempty α] (f : α → ℕ∞) (n : ℕ) :
     (⨆ x, f x = n) ↔ (∃ x, f x = n) ∧ (∀ y, f y ≤ n) := by
   constructor