Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case intro.intro
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
s✝ : Set F
hs : Set.Finite s✝
t : β
b : F
s : Set F
a✝¹ : b ∉ s
a✝ : Set.Finite s
X : Set E
ne_X : Set.Nonempty X
cX✝ : Convex ℝ X
kX : IsCompact X
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
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hs'Y : insert b s ⊆ Y
hb : b ∈ Y
X' : Set E := {x | x ∈ X ∧ f x b ≤ t}
X'_ne : Set.Nonempty X'
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : (∀ x ∈ X', ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
x : E
hx : x ∈ X'
y : F
hy : y ∈ insert b s
h : t < f x y
⊢ ∃ y ∈ s, t < f x y
Tactic:
rcases hy with (hy | hy)
Proof state after:
case intro.intro.inl
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
s✝ : Set F
hs : Set.Finite s✝
t : β
b : F
s : Set F
a✝¹ : b ∉ s
a✝ : Set.Finite s
X : Set E
ne_X : Set.Nonempty X
cX✝ : Convex ℝ X
kX : IsCompact X
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
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hs'Y : insert b s ⊆ Y
hb : b ∈ Y
X' : Set E := {x | x ∈ X ∧ f x b ≤ t}
X'_ne : Set.Nonempty X'
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : (∀ x ∈ X', ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
x : E
hx : x ∈ X'
y : F
h : t < f x y
hy : y = b
⊢ ∃ y ∈ s, t < f x y

case intro.intro.inr
β : Type u_3
E : Type u_2
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module ℝ E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalAddGroup E
inst✝⁷ : ContinuousSMul ℝ E
F : Type u_1
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module ℝ F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : ContinuousSMul ℝ F
Y : Set F
ne_Y : Set.Nonempty Y
cY : Convex ℝ Y
kY : IsCompact Y
f : E → F → β
inst✝¹ : LinearOrder β
inst✝ : DenselyOrdered β
s✝ : Set F
hs : Set.Finite s✝
t : β
b : F
s : Set F
a✝¹ : b ∉ s
a✝ : Set.Finite s
X : Set E
ne_X : Set.Nonempty X
cX✝ : Convex ℝ X
kX : IsCompact X
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
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hs'Y : insert b s ⊆ Y
hb : b ∈ Y
X' : Set E := {x | x ∈ X ∧ f x b ≤ t}
X'_ne : Set.Nonempty X'
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
hrec : (∀ x ∈ X', ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
x : E
hx : x ∈ X'
y : F
h : t < f x y
hy : y ∈ s
⊢ ∃ y ∈ s, t < f x y