rw [iSup₂_le_iff]
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y