internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case 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
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✝¹ : LinearOrder β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : ∀ (x : ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 })), x ∉ J1 ∩ J2
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ y1 y2
this :
  ∀ (u v : Set ↑(segment ℝ y1 y2)), IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
h2 : univ ⊆ J2
⊢ ERealSion.C X f t y1 ⊆ ERealSion.C X f t' y1
Tactic:
apply monotone_C X Y f t t' ⟨y1, hy1⟩ htt'.le
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case intro.intro.intro.intro.refine_5
β : 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
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✝¹ : LinearOrder β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : J1 ∩ J2 = ∅
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ y1 y2
this :
  ∀ (u v : Set ↑(segment ℝ y1 y2)), IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
⊢ univ ∩ (J1 ∩ J2) = ∅
Tactic:
simp only [hJ1J2, inter_empty]
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case intro.intro.intro.intro.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
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✝¹ : LinearOrder β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : J1 ∩ J2 = ∅
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ y1 y2
⊢ IsPreconnected (segment ℝ y1 y2)
Tactic:
exact Convex.isPreconnected (convex_segment y1 y2)
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case intro.intro.intro.intro.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
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✝¹ : LinearOrder β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : ∀ (x : ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 })), x ∉ J1 ∩ J2
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ y1 y2
this :
  ∀ (u v : Set ↑(segment ℝ y1 y2)), IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
⊢ IsClosed J1
Tactic:
exact isClosed_J X ne_X kX Y cY f hfx hfx' hfy hfy' a t t' ⟨y1, hy1⟩ ⟨y2, hy2⟩ ha' hinfi_le ht' htt'
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case intro.intro.intro.intro.refine_3
β : 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
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✝¹ : LinearOrder β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : ∀ (x : ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 })), x ∉ J1 ∩ J2
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ y1 y2
this :
  ∀ (u v : Set ↑(segment ℝ y1 y2)), IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
ha' : ∀ x ∈ X, f a y2 ⊔ f a y1 ≤ f x y2 ⊔ f x y1
ht' : t' < f a y2 ⊔ f a y1
⊢ IsClosed (ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 })
Tactic:
refine isClosed_J X ne_X kX Y cY f hfx hfx' hfy hfy' a t t' ⟨y2, hy2⟩ ⟨y1, hy1⟩ ha' hinfi_le ht' htt'
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case intro.intro.intro.intro.refine_4.mk.intro.mk.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
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✝¹ : LinearOrder β
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
y1 : F
hy1 : y1 ∈ Y
y2 : F
hy2 : y2 ∈ Y
t : β
ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
ha' : ∀ x ∈ X, f a y1 ⊔ f a y2 ≤ f x y1 ⊔ f x y2
t' : β
htt' : t < t'
ht' : t' < f a y1 ⊔ f a y2
J1 : Set ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }) :=
  ERealSion.J X Y f t t' { val := y1, property := hy1 } { val := y2, property := hy2 }
mem_J1_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
φ : ↑(segment ℝ y1 y2) ≃ₜ ↑(segment ℝ y2 y1) := Homeomorph.subtype (Homeomorph.refl F) ⋯
J2 : Set ↑(segment ℝ y1 y2) :=
  ⇑φ ⁻¹' ERealSion.J X Y f t t' { val := y2, property := hy2 } { val := y1, property := hy1 }
mem_J2_iff :
  ∀ (z : F) (hz : z ∈ segment ℝ y1 y2), { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hJ1J2 : ∀ (x : ↑(segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 })), x ∉ J1 ∩ J2
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ y1 y2
this :
  ∀ (u v : Set ↑(segment ℝ y1 y2)), IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
z : F
hz' : z ∈ segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }
hz'' : { val := z, property := hz' } ∈ J1 ∪ J2
hz : ↑{ val := z, property := hz' } ∈ segment ℝ y1 y2
a✝ : { val := ↑{ val := z, property := hz' }, property := hz } ∈ univ
⊢ { val := ↑{ val := z, property := hz' }, property := hz } ∈ J1 ∪ J2
Tactic:
exact hz''
Proof state after:
no goals
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
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✝¹ : LinearOrder β
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
s : Set F
hs : Set.Finite s
t : β
ht : ∀ x ∈ X, ∃ y ∈ s, t < f x y
⊢ s ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
revert X
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 : β
⊢ ∀ (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
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
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
Tactic:
intro X ne_X _ _ _ _ _ _
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
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
⊢ (∀ x ∈ X, ∃ y ∈ ∅, t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
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
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
⊢ (∀ x ∈ X, ∃ y ∈ ∅, t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
obtain ⟨x, hx⟩ := id ne_X
Proof state after:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
⊢ (∀ x ∈ X, ∃ y ∈ ∅, t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
⊢ (∀ x ∈ X, ∃ y ∈ ∅, t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
simp only [biInf_const ne_X, mem_empty_iff_false, ciSup_false, ciSup_const,
  not_lt_bot, IsEmpty.forall_iff]
Proof state after:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
⊢ (∀ x ∈ X, ∃ y, False ∧ t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
⊢ (∀ x ∈ X, ∃ y, False ∧ t < f x y) → ∅ ⊆ Y → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
simp only [false_and, exists_const, imp_false, empty_subset, forall_true_left]
Proof state after:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
⊢ (∀ (x : E), x ∉ X) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_finite
Proof state before:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
⊢ (∀ (x : E), x ∉ X) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
Tactic:
intro h
Proof state after:
case refine'_1.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 : β
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
x : E
hx : x ∈ X
h : ∀ (x : E), x ∉ X
⊢ ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0