Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
β : 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 : β
⊢ ∀ (X : Set E),
    Set.Nonempty X →
      Convex ℝ X →
        IsCompact X →
          (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
            (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
              (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                  (∀ x ∈ X, ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
refine' Set.Finite.induction_on hs _ _
Proof state after:
case refine'_1
β : 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 : β
⊢ ∀ (X : Set E),
    Set.Nonempty X →
      Convex ℝ X →
        IsCompact X →
          (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
            (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
              (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                  (∀ x ∈ X, ∃ y ∈ ∅, t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0

case refine'_2
β : 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 : β
⊢ ∀ {a : F} {s : Set F},
    a ∉ s →
      Set.Finite s →
        (∀ (X : Set E),
            Set.Nonempty X →
              Convex ℝ X →
                IsCompact X →
                  (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                    (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                          (∀ x ∈ X, ∃ y ∈ s, t < f x y) → s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0) →
          ∀ (X : Set E),
            Set.Nonempty X →
              Convex ℝ X →
                IsCompact X →
                  (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                    (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
                        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
                          (∀ x ∈ X, ∃ y ∈ insert a s, t < f x y) → insert a s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0