internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
case right
β : Type u_3
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 → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
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
hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X
a : E
ha : a ∈ X
ha' : ⨆ y ∈ Y, f a y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y
husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
b : F
hb : b ∈ Y
hb' : ⨅ x ∈ X, f x b = ⨆ x ∈ Y, ⨅ x_1 ∈ X, f x_1 x
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨅ x ∈ X, f x b
Tactic:
rw [minimax X ne_X cX kX Y cY f hfx hfx' hfy hfy']
Proof state after:
case right
β : Type u_3
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 → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
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
hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X
a : E
ha : a ∈ X
ha' : ⨆ y ∈ Y, f a y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y
husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
b : F
hb : b ∈ Y
hb' : ⨅ x ∈ X, f x b = ⨆ x ∈ Y, ⨅ x_1 ∈ X, f x_1 x
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, f x b
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
case right
β : Type u_3
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 → β
inst✝¹ : CompleteLinearOrder β
inst✝ : DenselyOrdered β
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
hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X
a : E
ha : a ∈ X
ha' : ⨆ y ∈ Y, f a y = ⨅ x ∈ X, ⨆ y ∈ Y, f x y
husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
b : F
hb : b ∈ Y
hb' : ⨅ x ∈ X, f x b = ⨆ x ∈ Y, ⨅ x_1 ∈ X, f x_1 x
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, f x b
Tactic:
rw [← hb']
Proof state after:
no goals
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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'
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof 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
Theorem: Sion.existsSaddlePointOn
Proof 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]
Proof 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)
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof state after:
no goals
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof state after:
no goals
Theorem: Sion.existsSaddlePointOn
Proof 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
Proof state after:
no goals