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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
obtain ⟨y0, hy0, ht0⟩ := exists_lt_iInf_of_lt_iInf_of_finite
  X ne_X cX kX Y cY f hfx hfx' hfy hfy' hs hst hsY
Proof state after:
case intro.intro
β : 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Theorem: ERealSion.minimax
Proof state before:
case intro.intro
β : 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Tactic:
simp only [lt_iSup_iff, exists_prop]
Proof state after:
case intro.intro
β : 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ ∃ i ∈ Y, t < ⨅ x ∈ X, f x i
Theorem: ERealSion.minimax
Proof state before:
case intro.intro
β : 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ ∃ i ∈ Y, t < ⨅ x ∈ X, f x i
Tactic:
use y0, hy0
Proof state after:
case 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨅ x ∈ X, f x y0
Theorem: ERealSion.minimax
Proof state before:
case 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
⊢ t < ⨅ x ∈ X, f x y0
Tactic:
obtain ⟨a, ha, h⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact
  ne_X kX (hfy y0 hy0)
Proof state after:
case right.intro.intro
β : 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
a : E
ha : a ∈ X
h : ∀ x ∈ X, f a y0 ≤ f x y0
⊢ t < ⨅ x ∈ X, f x y0
Theorem: ERealSion.minimax
Proof state before:
case right.intro.intro
β : 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}
s : Set F
hsY : s ⊆ Y
hs : Set.Finite s
hes : ⋂ y ∈ s, X' y = ∅
hst : ∀ x ∈ X, ∃ y ∈ s, t < f x y
y0 : F
hy0 : y0 ∈ Y
ht0 : ∀ x ∈ X, t < f x y0
a : E
ha : a ∈ X
h : ∀ x ∈ X, f a y0 ≤ f x y0
⊢ t < ⨅ x ∈ X, f x y0
Tactic:
exact lt_of_lt_of_le (ht0 a ha) (le_iInf₂_iff.mpr h)
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
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
let v : Y → Set E := fun y ↦ Exists.choose (hfyt y)
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 ⋯
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
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 ⋯
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
have hv : ∀ y, IsClosed (v y) ∧ X' y = X ∩ v y := fun y ↦ (hfyt y).choose_spec
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
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
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 : ?m.390150
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
obtain ⟨s, hs⟩ := kX.elim_finite_subfamily_closed v (fun y => (hv y).1) hsZ
Proof state after:
case intro
β : 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 ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Theorem: ERealSion.minimax
Proof state before:
case intro
β : 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 ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
have hs_ne : s.Nonempty := by
  rw [Finset.nonempty_iff_ne_empty]
  intro hs_e
  simp only [hs_e, Finset.not_mem_empty, iInter_of_empty, iInter_univ, inter_univ] at hs
  rw [Set.nonempty_iff_ne_empty] at ne_X
  exact ne_X hs
Proof state after:
case intro
β : 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
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Theorem: ERealSion.minimax
Proof state before:
case intro
β : 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
⊢ ∃ s ⊆ Y, Set.Finite s ∧ ⋂ y ∈ s, X' y = ∅
Tactic:
use (Subtype.val : Y → F) '' (s : Set Y)
Proof state after:
case h
β : 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 ∧ Set.Finite (Subtype.val '' ↑s) ∧ ⋂ y ∈ Subtype.val '' ↑s, X' y = ∅
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.Nonempty
Tactic:
rw [Finset.nonempty_iff_ne_empty]
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 = ∅
⊢ s ≠ ∅