Theorem: Sion.existsSaddlePointOn (Sion/Sion.lean)

State before:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
let φ : E → F → EReal := fun x y ↦ (f x y).toEReal
State after:
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)
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

State before:
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)
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
have hφx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ φ x y) Y := fun x hx ↦
  continuous_coe_real_ereal.comp_upperSemicontinuousOn (hfx x hx) EReal.coe_strictMono.monotone
State after:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

State before:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
have hφx' : ∀ (x : E), x ∈ X → QuasiconcaveOn ℝ Y fun y ↦ φ x y := fun x hx ↦
  by convert (hfx' x hx).monotone_comp EReal.coe_strictMono.monotone
State after:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

State before:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
have hφy : ∀ (y : F), y ∈ Y → LowerSemicontinuousOn (fun x ↦ φ x y) X := fun y hy ↦
  continuous_coe_real_ereal.comp_lowerSemicontinuousOn (hfy y hy) EReal.coe_strictMono.monotone
State after:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

State before:
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
have hφy': ∀ (y : F), y ∈ Y → QuasiconvexOn ℝ X fun x ↦ φ x y := fun y hy ↦
  by convert (hfy' y hy).monotone_comp EReal.coe_strictMono.monotone
State after:
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 ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

State before:
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 ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
obtain ⟨a, ha, b, hb, hab⟩ :=
  ERealSion.exists_saddlePointOn X ne_X cX kX Y ne_Y cY kY φ hφx hφx' hφy hφy'
State after:
case intro.intro.intro.intro
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b

State before:
case intro.intro.intro.intro
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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
use a, ha, b, hb
State after:
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
⊢ IsSaddlePointOn X Y f a b

State before:
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
⊢ IsSaddlePointOn X Y f a b
Tactic:
intro x hx y hy
State after:
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

State before:
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
Tactic:
simp only [← EReal.coe_le_coe_iff]
State after:
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)

State before:
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)
Tactic:
exact hab x hx y hy
State after:
no goals

State before:
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
x : E
hx : x ∈ X
⊢ QuasiconcaveOn ℝ Y fun y => φ x y
Tactic:
convert (hfx' x hx).monotone_comp EReal.coe_strictMono.monotone
State after:
no goals

State before:
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
y : F
hy : y ∈ Y
⊢ QuasiconvexOn ℝ X fun x => φ x y
Tactic:
convert (hfy' y hy).monotone_comp EReal.coe_strictMono.monotone
State after:
no goals