Theorem: ERealSion.C_subset_or (Sion/Sion.lean)

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
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, f a ↑y ⊔ f a ↑y' ≤ f x ↑y ⊔ f x ↑y'
hb : b < f a ↑y ⊔ f a ↑y'
z : ↑(segment ℝ ↑y ↑y')
⊢ ERealSion.C X f b ↑z ⊆ ERealSion.C X f b ↑y ∨ ERealSion.C X f b ↑z ⊆ ERealSion.C X f b ↑y'
Tactic:
apply isPreconnected_iff_subset_of_disjoint_closed.mp
  (isPreconnected_C X Y f hfy' b ⟨z, cY.segment_subset y.prop y'.prop z.prop⟩)
  _ _ (isClosed_C X Y f hfy b y) (isClosed_C X Y f hfy b y')
  (C_subset_union X Y f hfx' b y y' z)
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
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
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, f a ↑y ⊔ f a ↑y' ≤ f x ↑y ⊔ f x ↑y'
hb : b < f a ↑y ⊔ f a ↑y'
z : ↑(segment ℝ ↑y ↑y')
⊢ ERealSion.C X f b ↑{ val := ↑z, property := ⋯ } ∩ (ERealSion.C X f b ↑y ∩ ERealSion.C X f b ↑y') = ∅

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
a : E
b : β
y y' : ↑Y
ha : ∀ x ∈ X, f a ↑y ⊔ f a ↑y' ≤ f x ↑y ⊔ f x ↑y'
hb : b < f a ↑y ⊔ f a ↑y'
z : ↑(segment ℝ ↑y ↑y')
⊢ ERealSion.C X f b ↑{ val := ↑z, property := ⋯ } ∩ (ERealSion.C X f b ↑y ∩ ERealSion.C X f b ↑y') = ∅
Tactic:
rw [Set.disjoint_iff_inter_eq_empty.mp (disjoint_C X Y f a b y y' ha hb),
  Set.inter_empty]
State after:
no goals