internlm/Lean-Github huggingface dataset:
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
hsZ : X ∩ ⋂ i, v i = ∅
s : Finset ↑Y
hs : X ∩ ⋂ i ∈ s, v i = ∅
⊢ s ≠ ∅
Tactic:
intro hs_e
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 : 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 ∩ ⋂ i ∈ s, v i = ∅
hs_e : s = ∅
⊢ 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 : 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 ∩ ⋂ i ∈ s, v i = ∅
hs_e : s = ∅
⊢ False
Tactic:
simp only [hs_e, Finset.not_mem_empty, iInter_of_empty, iInter_univ, inter_univ] at hs
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 : 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_e : s = ∅
hs : X = ∅
⊢ 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 : 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_e : s = ∅
hs : X = ∅
⊢ False
Tactic:
rw [Set.nonempty_iff_ne_empty] at ne_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 : 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_e : s = ∅
hs : X = ∅
⊢ 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 : 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_e : s = ∅
hs : X = ∅
⊢ False
Tactic:
exact ne_X hs
Proof state after:
no goals
Theorem: ERealSion.minimax
Proof state before:
case h.left
β : 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 ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Subtype.val '' ↑s ⊆ Y
Tactic:
exact Subtype.coe_image_subset Y ↑s
Proof state after:
no goals
Theorem: ERealSion.minimax
Proof state before:
case h.right.left
β : 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 ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ Set.Finite (Subtype.val '' ↑s)
Tactic:
apply s.finite_toSet.image
Proof state after:
no goals
Theorem: ERealSion.minimax
Proof state before:
case h.right.right
β : 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 ∩ ⋂ i ∈ s, v i = ∅
hs_ne : s.Nonempty
⊢ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem] at hs ⊢
Proof state after:
case h.right.right
β : 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), x ∉ ⋂ y ∈ Subtype.val '' ↑s, X' y
Theorem: ERealSion.minimax
Proof state before:
case h.right.right
β : 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), x ∉ ⋂ y ∈ Subtype.val '' ↑s, X' y
Tactic:
intro x hx
Proof state after:
case h.right.right
β : 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 : x ∈ ⋂ y ∈ Subtype.val '' ↑s, X' y
⊢ False
Theorem: ERealSion.minimax
Proof state before:
case h.right.right
β : 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 : x ∈ ⋂ y ∈ Subtype.val '' ↑s, X' y
⊢ False
Tactic:
simp only [mem_image, Finset.mem_coe, SetCoe.exists, Subtype.coe_mk, exists_and_right,
  exists_eq_right, iInf_eq_iInter, iInter_exists, mem_iInter, mem_sep_iff] at hx
Proof state after:
case h.right.right
β : 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
⊢ False
Theorem: ERealSion.minimax
Proof state before:
case h.right.right
β : 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
⊢ False
Tactic:
apply hs x
Proof state after:
case h.right.right
β : 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
⊢ x ∈ X ∩ ⋂ i ∈ s, v i
Theorem: ERealSion.minimax
Proof state before:
case h.right.right
β : 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
⊢ x ∈ X ∩ ⋂ i ∈ s, v i
Tactic:
rw [iInter_coe_set, mem_inter_iff, mem_iInter]
Proof state after:
case h.right.right
β : 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
⊢ x ∈ X ∧ ∀ (i : F), x ∈ ⋂ (h : i ∈ Y), ⋂ (_ : { val := i, property := h } ∈ s), v { val := i, property := h }