internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.minimax
Proof state before:
case h.right.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 : 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
Tactic:
obtain ⟨⟨j, hj⟩, hjs⟩ := hs_ne
Proof state after:
case h.right.right.left.intro.mk
β : 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
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
j : F
hj : j ∈ Y
hjs : { val := j, property := hj } ∈ s
⊢ x ∈ X
Theorem: ERealSion.minimax
Proof state before:
case h.right.right.left.intro.mk
β : 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
x : E
hx : ∀ (i : F) (i_1 : i ∈ Y), { val := i, property := ⋯ } ∈ s → x ∈ X' i
j : F
hj : j ∈ Y
hjs : { val := j, property := hj } ∈ s
⊢ x ∈ X
Tactic:
exact (hx j hj hjs).1
Proof state after:
no goals
Theorem: ERealSion.minimax
Proof state before:
case h.right.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
⊢ ∀ (i : F), x ∈ ⋂ (h : i ∈ Y), ⋂ (_ : { val := i, property := h } ∈ s), v { val := i, property := h }
Tactic:
intro y
Proof state after:
case h.right.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
y : F
⊢ x ∈ ⋂ (h : y ∈ Y), ⋂ (_ : { val := y, property := h } ∈ s), v { val := y, property := h }
Theorem: ERealSion.minimax
Proof state before:
case h.right.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
y : F
⊢ x ∈ ⋂ (h : y ∈ Y), ⋂ (_ : { val := y, property := h } ∈ s), v { val := y, property := h }
Tactic:
rw [mem_iInter]
Proof state after:
case h.right.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
y : F
⊢ ∀ (i : y ∈ Y), x ∈ ⋂ (_ : { val := y, property := i } ∈ s), v { val := y, property := i }
Theorem: ERealSion.minimax
Proof state before:
case h.right.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
y : F
⊢ ∀ (i : y ∈ Y), x ∈ ⋂ (_ : { val := y, property := i } ∈ s), v { val := y, property := i }
Tactic:
intro hy
Proof state after:
case h.right.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
y : F
hy : y ∈ Y
⊢ x ∈ ⋂ (_ : { val := y, property := hy } ∈ s), v { val := y, property := hy }
Theorem: ERealSion.minimax
Proof state before:
case h.right.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
y : F
hy : y ∈ Y
⊢ x ∈ ⋂ (_ : { val := y, property := hy } ∈ s), v { val := y, property := hy }
Tactic:
rw [mem_iInter]
Proof state after:
case h.right.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
y : F
hy : y ∈ Y
⊢ { val := y, property := hy } ∈ s → x ∈ v { val := y, property := hy }
Theorem: ERealSion.minimax
Proof state before:
case h.right.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
y : F
hy : y ∈ Y
⊢ { val := y, property := hy } ∈ s → x ∈ v { val := y, property := hy }
Tactic:
intro hy'
Proof state after:
case h.right.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
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ v { val := y, property := hy }
Theorem: ERealSion.minimax
Proof state before:
case h.right.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
y : F
hy : y ∈ Y
hy' : { val := y, property := hy } ∈ s
⊢ x ∈ v { val := y, property := hy }
Tactic:
apply Set.inter_subset_right X
Proof state after:
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 ∩ v { val := y, property := hy }
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 ∩ v { val := y, property := hy }
Tactic:
rw [← (hv (⟨y, hy⟩ : Y)).2]
Proof state after:
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' ↑{ val := y, property := hy }
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' ↑{ val := y, property := hy }
Tactic:
simp only [Subtype.coe_mk, mem_sep_iff]
Proof state after:
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