exact hab x hx y hy
case right
E : Type u_1
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalAddGroup E
inst✝⁵ : ContinuousSMul ℝ E
F : Type u_2
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
X : Set E
ne_X : Set.Nonempty X
cX : Convex ℝ X
kX : IsCompact X
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → ℝ
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
φ : E → F → EReal := fun x y => ↑(f x y)
hφx : ∀ x ∈ X, UpperSemicontinuousOn (fun y => φ x y) Y
hφx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => φ x y
hφy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => φ x y) X
hφy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => φ x y
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
hab : IsSaddlePointOn X Y φ a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ ↑(f a y) ≤ ↑(f x b)
no goals