Sum of suprema in ENat

@[simp]

theorem ENat.toNat_prod {ι : Type u_2} {s : Finset ι} {f : ι → ℕ∞} : (∏ i ∈ s, f i).toNat = ∏ i ∈ s, (f i).toNat

theorem ENat.iInf_sum {ι : Type u_2} {α : Type u_3} {f : ι → α → ℕ∞} {s : Finset α} [Nonempty ι] (h : ∀ (t : Finset α) (i j : ι), ∃ (k : ι), ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a) : ⨅ (i : ι), ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ (i : ι), f i a

theorem ENat.prod_ne_top {α : Type u_1} {s : Finset α} {f : α → ℕ∞} (h : ∀ a ∈ s, f a ≠ ⊤) : ∏ a ∈ s, f a ≠ ⊤

A product of finite numbers is still finite.

theorem ENat.prod_lt_top {α : Type u_1} {s : Finset α} {f : α → ℕ∞} (h : ∀ a ∈ s, f a < ⊤) : ∏ a ∈ s, f a < ⊤

A product of finite numbers is still finite.

@[simp]

theorem ENat.sum_eq_top {α : Type u_1} {s : Finset α} {f : α → ℕ∞} : ∑ x ∈ s, f x = ⊤ ↔ ∃ a ∈ s, f a = ⊤

A sum is infinite iff one of the summands is infinite.

theorem ENat.sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ℕ∞} : ∑ a ∈ s, f a ≠ ⊤ ↔ ∀ a ∈ s, f a ≠ ⊤

A sum is finite iff all summands are finite.

@[simp]

theorem ENat.sum_lt_top {α : Type u_1} {s : Finset α} {f : α → ℕ∞} : ∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤

A sum is finite iff all summands are finite.

theorem ENat.lt_top_of_sum_ne_top {α : Type u_1} {s : Finset α} {f : α → ℕ∞} (h : ∑ x ∈ s, f x ≠ ⊤) {a : α} (ha : a ∈ s) : f a < ⊤

theorem ENat.toNat_sum {α : Type u_1} {s : Finset α} {f : α → ℕ∞} (hf : ∀ a ∈ s, f a ≠ ⊤) : (∑ a ∈ s, f a).toNat = ∑ a ∈ s, (f a).toNat

Seeing ℕ∞ as ℕ does not change their sum, unless one of the ℕ∞ is infinity

theorem ENat.sum_lt_sum_of_nonempty {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f g : α → ℕ∞} (Hlt : ∀ i ∈ s, f i < g i) : ∑ i ∈ s, f i < ∑ i ∈ s, g i

theorem ENat.exists_le_of_sum_le {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {f g : α → ℕ∞} (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) : ∃ i ∈ s, f i ≤ g i

theorem ENat.sum_iSup {α : Type u_1} {ι : Type u_2} {s : Finset α} {f : α → ι → ℕ∞} (hf : ∀ (i j : ι), ∃ (k : ι), ∀ (a : α), f a i ≤ f a k ∧ f a j ≤ f a k) : ∑ a ∈ s, ⨆ (i : ι), f a i = ⨆ (i : ι), ∑ a ∈ s, f a i

theorem ENat.sum_iSup_of_monotone {α : Type u_1} {ι : Type u_2} [Preorder ι] [IsDirectedOrder ι] {s : Finset α} {f : α → ι → ℕ∞} (hf : ∀ (a : α), Monotone (f a)) : ∑ a ∈ s, iSup (f a) = ⨆ (n : ι), ∑ a ∈ s, f a n