specialize hfx' ⟨y.prop, inf_le_left⟩ ⟨y'.prop, inf_le_right⟩ z.prop
β : 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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hfx' :
  ∀ ⦃x_1 : F⦄,
    x_1 ∈ {x_2 | x_2 ∈ Y ∧ f ↑x ↑y ⊓ f ↑x ↑y' ≤ (fun y => f (↑x) y) x_2} →
      ∀ ⦃y_1 : F⦄,
        y_1 ∈ {x_2 | x_2 ∈ Y ∧ f ↑x ↑y ⊓ f ↑x ↑y' ≤ (fun y => f (↑x) y) x_2} →
          segment ℝ x_1 y_1 ⊆ {x_2 | x_2 ∈ Y ∧ f ↑x ↑y ⊓ f ↑x ↑y' ≤ (fun y => f (↑x) y) x_2}
⊢ f ↑x ↑y ⊓ f ↑x ↑y' ≤ b
β : 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
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
hfx' : ↑z ∈ {x_1 | x_1 ∈ Y ∧ f ↑x ↑y ⊓ f ↑x ↑y' ≤ (fun y => f (↑x) y) x_1}
⊢ f ↑x ↑y ⊓ f ↑x ↑y' ≤ b