internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case h
β : 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
hrec :
  ∀ (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
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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
⊢ IsClosed (Subtype.val ⁻¹' X')
Tactic:
rw [inducing_subtype_val.isClosed_iff]
Proof state after:
case h
β : 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
hrec :
  ∀ (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
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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
⊢ ∃ t, IsClosed t ∧ Subtype.val ⁻¹' t = Subtype.val ⁻¹' X'
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case h
β : 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
hrec :
  ∀ (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
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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
⊢ ∃ t, IsClosed t ∧ Subtype.val ⁻¹' t = Subtype.val ⁻¹' X'
Tactic:
specialize hfy b hb
Proof state after:
case h
β : 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
hrec :
  ∀ (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
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, 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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
hfy : LowerSemicontinuousOn (fun x => f x b) X
⊢ ∃ t, IsClosed t ∧ Subtype.val ⁻¹' t = Subtype.val ⁻¹' X'
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case h
β : 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
hrec :
  ∀ (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
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, 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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
hfy : LowerSemicontinuousOn (fun x => f x b) X
⊢ ∃ t, IsClosed t ∧ Subtype.val ⁻¹' t = Subtype.val ⁻¹' X'
Tactic:
rw [lowerSemicontinuousOn_iff_preimage_Iic] at hfy
Proof state after:
case h
β : 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
hrec :
  ∀ (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
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, 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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
hfy : ∀ (b_1 : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x b) ⁻¹' Iic b_1 = X ∩ v
⊢ ∃ t, IsClosed t ∧ Subtype.val ⁻¹' t = Subtype.val ⁻¹' X'
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case right.h
β : 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
hrec :
  ∀ (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
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, 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
this : X' = Subtype.val '' (Subtype.val ⁻¹' X')
kX' : CompactSpace ↑X
hfy : ∀ (b_1 : β), ∃ v, IsClosed v ∧ X ∩ (fun x => f x b) ⁻¹' Iic b_1 = X ∩ v
v : Set E
hv : IsClosed v
hv' : X ∩ (fun x => f x b) ⁻¹' Iic t = X ∩ v
x : E
⊢ x ∈ X ∩ (fun x => f x b) ⁻¹' Iic t ↔ x ∈ X ∩ X'
Tactic:
simp only [mem_inter_iff, mem_preimage, mem_Iic, mem_setOf_eq, and_self_left, X']
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_2.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
hrec :
  ∀ (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
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'
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
specialize hrec X' X'_ne cX' kX'
      (fun x hx' ↦ hfx x (hX'X hx'))
      (fun x hx' ↦ hfx' x (hX'X hx'))
      (fun y hy ↦ LowerSemicontinuousOn.mono (hfy y hy) hX'X)
      (fun y hy ↦ cX'.quasiconvexOn_restrict (hfy' y hy) hX'X)
Proof state after:
case refine'_2.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
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_2.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
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
obtain ⟨y1, hy1, hty1⟩ := hrec  ht_lt (subset_trans (subset_insert b s) hs'Y)
Proof state after:
case refine'_2.inr.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
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_2.inr.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
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
apply exists_lt_iInf_of_lt_iInf_of_sup X ne_X kX Y cY f hfx hfx' hfy hfy' hb hy1
Proof state after:
case refine'_2.inr.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
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
⊢ ∀ x ∈ X, t < f x b ⊔ f x y1
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_2.inr.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
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
⊢ ∀ x ∈ X, t < f x b ⊔ f x y1
Tactic:
intro x hx
Proof state after:
case refine'_2.inr.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
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
⊢ t < f x b ⊔ f x y1
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 : β
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 ∈ X', ∃ y ∈ s, t < f x y
Tactic:
intro x hx
Proof state after:
β : 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 ∈ s, t < f x y