Diagonal suprema

A supremum over two indices of a family monotone in both is the supremum along the diagonal. [UPSTREAM] candidate for Mathlib/Order/CompleteLattice/Basic.lean, beside iSup_iSup_eq_left.

theorem iSup_iSup_eq_iSup_diag {L : Type u_1} [CompleteLattice L] {g : ℕ → ℕ → L} (hg : ∀ (m n m' n' : ℕ), m ≤ m' → n ≤ n' → g m n ≤ g m' n') : ⨆ (m : ℕ), ⨆ (n : ℕ), g m n = ⨆ (n : ℕ), g n n

For a family monotone in both indices, the double supremum is the diagonal supremum.