Theorem: iSup₂_iInf₂_le_iInf₂_iSup₂ (Sion/Sion.lean)

State before:
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
Tactic:
rw [iSup₂_le_iff]
State after:
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

State before:
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
Tactic:
intro y hy
State after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

State before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
rw [le_iInf₂_iff]
State after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y

State before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y
Tactic:
intro x hx
State after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f x y

State before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f x y
Tactic:
exact iInf₂_le_of_le x hx (le_iSup₂_of_le y hy (le_refl _))
State after:
no goals