internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.disjoint_C
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
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'
⊢ Disjoint (ERealSion.C X f b ↑y) (ERealSion.C X f b ↑y')
Tactic:
rw [Set.disjoint_iff]
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
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'
⊢ ERealSion.C X f b ↑y ∩ ERealSion.C X f b ↑y' ⊆ ∅
Theorem: ERealSion.disjoint_C
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
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'
⊢ ERealSion.C X f b ↑y ∩ ERealSion.C X f b ↑y' ⊆ ∅
Tactic:
rintro ⟨x, hx⟩ ⟨hx1, hx2⟩
Proof state after:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ { val := x, property := hx } ∈ ∅
Theorem: ERealSion.disjoint_C
Proof state before:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ { val := x, property := hx } ∈ ∅
Tactic:
simp only [mem_empty_iff_false]
Proof state after:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ False
Theorem: ERealSion.disjoint_C
Proof state before:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ False
Tactic:
apply not_le_of_lt hb
Proof state after:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ f a ↑y ⊔ f a ↑y' ≤ b
Theorem: ERealSion.disjoint_C
Proof state before:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ f a ↑y ⊔ f a ↑y' ≤ b
Tactic:
apply le_trans (ha x hx)
Proof state after:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ f x ↑y ⊔ f x ↑y' ≤ b
Theorem: ERealSion.disjoint_C
Proof state before:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ f x ↑y ⊔ f x ↑y' ≤ b
Tactic:
simp only [sup_le_iff]
Proof state after:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ f x ↑y ≤ b ∧ f x ↑y' ≤ b
Theorem: ERealSion.disjoint_C
Proof state before:
case 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
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'
x : E
hx : x ∈ X
hx1 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y
hx2 : { val := x, property := hx } ∈ ERealSion.C X f b ↑y'
⊢ f x ↑y ≤ b ∧ f x ↑y' ≤ b
Tactic:
exact ⟨hx1, hx2⟩
Proof state after:
no goals
Theorem: ERealSion.C_subset_union
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
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
⊢ x ∈ ERealSion.C X f b ↑y ∪ ERealSion.C X f b ↑y'
Tactic:
simp only [Set.mem_union, mem_C_iff, ← inf_le_iff]
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
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
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
⊢ f ↑x ↑y ⊓ f ↑x ↑y' ≤ b
Theorem: ERealSion.C_subset_union
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
b : β
y y' : ↑Y
z : ↑(segment ℝ ↑y ↑y')
x : ↑X
hx : x ∈ ERealSion.C X f b ↑z
⊢ f ↑x ↑y ⊓ f ↑x ↑y' ≤ b
Tactic:
specialize hfx' x x.2 (f x y ⊓ f x y')
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
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' : Convex ℝ {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
Theorem: ERealSion.C_subset_union
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
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' : Convex ℝ {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
Tactic:
rw [convex_iff_segment_subset] at hfx'
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
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
Theorem: ERealSion.C_subset_union
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
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
Tactic:
specialize hfx' ⟨y.prop, inf_le_left⟩ ⟨y'.prop, inf_le_right⟩ z.prop
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
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
Theorem: ERealSion.C_subset_union
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
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
Tactic:
exact le_trans hfx'.2 hx
Proof state after:
no goals
Theorem: ERealSion.C_subset_or
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
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)
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
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') = ∅