From f3b25b670fcc177c51495c7a0b6f4a0b7b288621 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 9 Oct 2024 09:03:28 +0000 Subject: [PATCH] remove bogus deprecated alias --- Mathlib/Data/ENat/Lattice.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/Data/ENat/Lattice.lean b/Mathlib/Data/ENat/Lattice.lean index c36a3b3f56e1b..50b5dd3009e51 100644 --- a/Mathlib/Data/ENat/Lattice.lean +++ b/Mathlib/Data/ENat/Lattice.lean @@ -209,9 +209,6 @@ lemma finsetSum_iSup_of_monotone {α ι : Type*} [Preorder ι] [IsDirected ι ( {f : α → ι → ℕ∞} (hf : ∀ a, Monotone (f a)) : (∑ a ∈ s, iSup (f a)) = ⨆ n, ∑ a ∈ s, f a n := finsetSum_iSup fun i j ↦ (exists_ge_ge i j).imp fun _k ⟨hi, hj⟩ a ↦ ⟨hf a hi, hf a hj⟩ -@[deprecated (since := "2024-07-14")] -alias finset_sum_iSup_nat := finsetSum_iSup_of_monotone - proof_wanted smul_iSup {R} [SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R) : c • ⨆ i, f i = ⨆ i, c • f i