internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.minimax
Proof state before:
case h.right.right.right.a
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : ∀ (x : E), x ∉ X ∩ ⋂ i ∈ s, v i
hs_ne : s.Nonempty
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ X' y
Tactic:
exact hx y hy hy'
Proof state after:
no goals
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : t < ⨅ x ∈ X, ⨆ y ∈ Y, f x y
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ X ∩ ⋂ i, v i = ∅
Tactic:
rw [← not_le] at ht
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ X ∩ ⋂ i, v i = ∅
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ X ∩ ⋂ i, v i = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem]
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ ∀ (x : E), x ∉ X ∩ ⋂ i, v i
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
⊢ ∀ (x : E), x ∉ X ∩ ⋂ i, v i
Tactic:
intro x hx
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ False
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ False
Tactic:
apply ht
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∩ ⋂ i, v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
Tactic:
rw [mem_inter_iff, mem_iInter] at hx
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
Tactic:
apply iInf₂_le_of_le x _ _
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ x ∈ X

β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ x ∈ X

β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t
Tactic:
exact hx.1
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ⨆ y ∈ Y, f x y ≤ t
Tactic:
simp only [iSup_le_iff]
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ∀ i ∈ Y, f x i ≤ t
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
⊢ ∀ i ∈ Y, f x i ≤ t
Tactic:
intro y hy
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ f x y ≤ t
Theorem: ERealSion.minimax
Proof state before:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ f x y ≤ t
Tactic:
suffices x ∈ X' y by
  exact this.2
Proof state after:
β : Type u_1
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_3
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
t : β
ht : ¬⨅ x ∈ X, ⨆ y ∈ Y, f x y ≤ t
X' : F → Set E := fun y => {x | x ∈ X ∧ f x y ≤ t}
hfyt : ∀ (y : ↑Y), ∃ vy, IsClosed vy ∧ X' ↑y = X ∩ vy
v : ↑Y → Set E := fun y => Exists.choose ⋯
hv : ∀ (y : ↑Y), IsClosed (v y) ∧ X' ↑y = X ∩ v y
x : E
hx : x ∈ X ∧ ∀ (i : ↑Y), x ∈ v i
y : F
hy : y ∈ Y
⊢ x ∈ X' y