internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
β : 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
x : E
hx : x ∈ X
⊢ ∀ i ∈ Y, LowerSemicontinuousWithinAt (fun x => f x i) X x
Tactic:
intro y hy
Proof state after:
β : 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
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ LowerSemicontinuousWithinAt (fun x => f x y) X x
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
β : 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
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ LowerSemicontinuousWithinAt (fun x => f x y) X x
Tactic:
exact hfy y hy x hx
Proof state after:
no goals
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
β : 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 ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
obtain ⟨a, ha, ha'⟩ := LowerSemicontinuousOn.exists_iInf_of_isCompact ne_X kX hlsc
Proof state after:
case intro.intro
β : 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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
case intro.intro
β : 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
⊢ ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
use a, ha
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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a 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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
suffices husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y by
  obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_iSup_of_isCompact ne_Y kY husc
  use b, hb
  rw [isSaddlePointOn_iff' ha hb]
  rw [ha']
  rw [minimax X ne_X cX kX Y cY f hfx hfx' hfy hfy']
  rw [← hb']
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
⊢ UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
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
⊢ UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y
Tactic:
intro y hy
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
y : F
hy : y ∈ Y
⊢ UpperSemicontinuousWithinAt (fun y => ⨅ x ∈ X, f x y) Y y
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
y : F
hy : y ∈ Y
⊢ UpperSemicontinuousWithinAt (fun y => ⨅ x ∈ X, f x y) Y y
Tactic:
apply upperSemicontinuousWithinAt_iInf₂ ne_X kX _ (hfy y hy)
Proof state after:
β : 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
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, UpperSemicontinuousWithinAt (f i) Y y
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
β : 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
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, UpperSemicontinuousWithinAt (f i) Y y
Tactic:
intro x hx
Proof state after:
β : 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
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ UpperSemicontinuousWithinAt (f x) Y y
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
β : 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
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ UpperSemicontinuousWithinAt (f x) Y y
Tactic:
exact hfx x hx y hy
Proof state after:
no goals
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
β : 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 ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_iSup_of_isCompact ne_Y kY husc
Proof state after:
case intro.intro
β : 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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Theorem: ERealSion.exists_saddlePointOn
Proof state before:
case intro.intro
β : 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
⊢ ∃ b ∈ Y, IsSaddlePointOn X Y f a b
Tactic:
use b, hb
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
⊢ IsSaddlePointOn X Y f a 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
⊢ IsSaddlePointOn X Y f a b
Tactic:
rw [isSaddlePointOn_iff' ha hb]
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, f a 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, f a y ≤ ⨅ x ∈ X, f x b
Tactic:
rw [ha']
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
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨅ x ∈ X, f x b