internlm/Lean-Github huggingface dataset:
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b
Tactic:
apply iInf₂_le a ha
Proof state after:
no goals
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨅ x ∈ X, f x b
Tactic:
apply le_trans _ h
Proof state after:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Theorem: isSaddlePointOn_iff'
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Tactic:
apply le_iSup₂ b hb
Proof state after:
no goals
Theorem: isSaddlePointOn_value
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Tactic:
rw [isSaddlePointOn_iff ha hb] at h
Proof state after:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Theorem: isSaddlePointOn_value
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b ∧ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Tactic:
constructor
Proof state after:
case left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b

case right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Theorem: isSaddlePointOn_value
Proof state before:
case left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y = f a b
Tactic:
apply le_antisymm
Proof state after:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b

case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Theorem: isSaddlePointOn_value
Proof state before:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ f a b
Tactic:
rw [← h.1]
Proof state after:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, f a y
Theorem: isSaddlePointOn_value
Proof state before:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ ⨆ y ∈ Y, f a y
Tactic:
exact le_trans (iInf₂_le a ha) (le_rfl)
Proof state after:
no goals
Theorem: isSaddlePointOn_value
Proof state before:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
rw [← h.2]
Proof state after:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Theorem: isSaddlePointOn_value
Proof state before:
case left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
apply iInf₂_mono
Proof state after:
case left.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ X, f i b ≤ ⨆ y ∈ Y, f i y
Theorem: isSaddlePointOn_value
Proof state before:
case left.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ X, f i b ≤ ⨆ y ∈ Y, f i y
Tactic:
intro x _
Proof state after:
case left.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
j✝ : x ∈ X
⊢ f x b ≤ ⨆ y ∈ Y, f x y
Theorem: isSaddlePointOn_value
Proof state before:
case left.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
j✝ : x ∈ X
⊢ f x b ≤ ⨆ y ∈ Y, f x y
Tactic:
apply le_iSup₂ b hb
Proof state after:
no goals
Theorem: isSaddlePointOn_value
Proof state before:
case right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y = f a b
Tactic:
apply le_antisymm
Proof state after:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b

case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Theorem: isSaddlePointOn_value
Proof state before:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ f a b
Tactic:
rw [← h.1]
Proof state after:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f a y
Theorem: isSaddlePointOn_value
Proof state before:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f a y
Tactic:
apply iSup₂_mono
Proof state after:
case right.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ f a i
Theorem: isSaddlePointOn_value
Proof state before:
case right.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ f a i
Tactic:
intro y _
Proof state after:
case right.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
y : F
j✝ : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ f a y
Theorem: isSaddlePointOn_value
Proof state before:
case right.a.h
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
y : F
j✝ : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ f a y
Tactic:
apply iInf₂_le a ha
Proof state after:
no goals
Theorem: isSaddlePointOn_value
Proof state before:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
rw [← h.2]
Proof state after:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Theorem: isSaddlePointOn_value
Proof state before:
case right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ ⨅ x ∈ X, f x b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
apply le_trans (le_rfl) (le_iSup₂ b hb)
Proof state after:
no goals
Theorem: ERealSion.mem_C_iff
Proof state before:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
y : ↑Y
x : ↑X
⊢ x ∈ ERealSion.C X f b ↑y ↔ f ↑x ↑y ≤ b
Tactic:
simp [C]
Proof state after:
no goals
Theorem: ERealSion.nonempty_C
Proof state before:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
y : ↑Y
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
⊢ Set.Nonempty (ERealSion.C X f b ↑y)
Tactic:
rcases y with ⟨y, hy⟩
Proof state after:
case mk
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
⊢ Set.Nonempty (ERealSion.C X f b ↑{ val := y, property := hy })
Theorem: ERealSion.nonempty_C
Proof state before:
case mk
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
⊢ Set.Nonempty (ERealSion.C X f b ↑{ val := y, property := hy })
Tactic:
obtain ⟨x, hx, hx_le⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact ne_X kX (hfy y hy)
Proof state after:
case mk.intro.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : ∀ x_1 ∈ X, f x y ≤ f x_1 y
⊢ Set.Nonempty (ERealSion.C X f b ↑{ val := y, property := hy })
Theorem: ERealSion.nonempty_C
Proof state before:
case mk.intro.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : ∀ x_1 ∈ X, f x y ≤ f x_1 y
⊢ Set.Nonempty (ERealSion.C X f b ↑{ val := y, property := hy })
Tactic:
obtain ⟨x', hx', hx'b⟩ := h y hy
Proof state after:
case mk.intro.intro.intro.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : ∀ x_1 ∈ X, f x y ≤ f x_1 y
x' : E
hx' : x' ∈ X
hx'b : f x' y ≤ b
⊢ Set.Nonempty (ERealSion.C X f b ↑{ val := y, property := hy })
Theorem: ERealSion.nonempty_C
Proof state before:
case mk.intro.intro.intro.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : ∀ x_1 ∈ X, f x y ≤ f x_1 y
x' : E
hx' : x' ∈ X
hx'b : f x' y ≤ b
⊢ Set.Nonempty (ERealSion.C X f b ↑{ val := y, property := hy })
Tactic:
exact ⟨⟨x, hx⟩, le_trans (hx_le x' hx') hx'b⟩
Proof state after:
no goals
Theorem: ERealSion.isClosed_C
Proof state before:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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
b : β
y : ↑Y
⊢ IsClosed (ERealSion.C X f b ↑y)
Tactic:
specialize hfy y.val y.prop
Proof state after:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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, QuasiconvexOn ℝ X fun x => f x y
b : β
y : ↑Y
hfy : LowerSemicontinuousOn (fun x => f x ↑y) X
⊢ IsClosed (ERealSion.C X f b ↑y)
Theorem: ERealSion.isClosed_C
Proof state before:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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, QuasiconvexOn ℝ X fun x => f x y
b : β
y : ↑Y
hfy : LowerSemicontinuousOn (fun x => f x ↑y) X
⊢ IsClosed (ERealSion.C X f b ↑y)
Tactic:
rw [lowerSemicontinuousOn_iff_restrict] at hfy
Proof state after:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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, QuasiconvexOn ℝ X fun x => f x y
b : β
y : ↑Y
hfy : LowerSemicontinuous (restrict X fun x => f x ↑y)
⊢ IsClosed (ERealSion.C X f b ↑y)
Theorem: ERealSion.isClosed_C
Proof state before:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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, QuasiconvexOn ℝ X fun x => f x y
b : β
y : ↑Y
hfy : LowerSemicontinuous (restrict X fun x => f x ↑y)
⊢ IsClosed (ERealSion.C X f b ↑y)
Tactic:
rw [lowerSemicontinuous_iff_isClosed_preimage] at hfy
Proof state after:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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, QuasiconvexOn ℝ X fun x => f x y
b : β
y : ↑Y
hfy : ∀ (y_1 : β), IsClosed ((restrict X fun x => f x ↑y) ⁻¹' Iic y_1)
⊢ IsClosed (ERealSion.C X f b ↑y)
Theorem: ERealSion.isClosed_C
Proof state before:
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
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✝¹ : LinearOrder β
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, QuasiconvexOn ℝ X fun x => f x y
b : β
y : ↑Y
hfy : ∀ (y_1 : β), IsClosed ((restrict X fun x => f x ↑y) ⁻¹' Iic y_1)
⊢ IsClosed (ERealSion.C X f b ↑y)
Tactic:
exact hfy b
Proof state after:
no goals