Sum of suprema in ENat

theorem ENat.sum_iSup {α : Type u_1} {ι : Type u_2} {s : Finset α} {f : α → ι → ENat} (hf : ∀ (i j : ι), Exists fun (k : ι) => ∀ (a : α), And (LE.le (f a i) (f a k)) (LE.le (f a j) (f a k))) : Eq (s.sum fun (a : α) => iSup fun (i : ι) => f a i) (iSup fun (i : ι) => s.sum fun (a : α) => f a i)

theorem ENat.sum_iSup_of_monotone {α : Type u_1} {ι : Type u_2} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => LE.le x1 x2] {s : Finset α} {f : α → ι → ENat} (hf : ∀ (a : α), Monotone (f a)) : Eq (s.sum fun (a : α) => iSup (f a)) (iSup fun (n : ι) => s.sum fun (a : α) => f a n)