Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case 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
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
h1 : univ ⊆ J1
⊢ { val := y2, property := ⋯ } ∈ J1 ∧ { val := y2, property := ⋯ } ∈ J2
Tactic:
refine ⟨h1 (Set.mem_univ _), ?_⟩
Proof state after:
case 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
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
h1 : univ ⊆ J1
⊢ { val := y2, property := ⋯ } ∈ J2