theorem iSup_eq_iSup {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [CompleteLattice α] {f : ι → α} {g : ι' → α} (h₀ : ∀ (i : ι), ∃ (j : ι'), f i ≤ g j) (h₁ : ∀ (j : ι'), ∃ (i : ι), g j ≤ f i) : ⨆ (i : ι), f i = ⨆ (j : ι'), g j