internlm/Lean-Github huggingface dataset:
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case hg
β : 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
⊢ LowerSemicontinuousOn (fun x => f x y2) X
Tactic:
exact hfy y2 hy2
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
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
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 }
z : F
x✝ : z ∈ segment ℝ y1 y2
⊢ { val := z, property := x✝ } ∈ J1 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
Tactic:
simp [J1, J]
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
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
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)
Tactic:
apply Homeomorph.subtype (Homeomorph.refl F)
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
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
⊢ ∀ (x : F), x ∈ segment ℝ y1 y2 ↔ (Homeomorph.refl F) x ∈ segment ℝ y2 y1
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
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
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
⊢ ∀ (x : F), x ∈ segment ℝ y1 y2 ↔ (Homeomorph.refl F) x ∈ segment ℝ y2 y1
Tactic:
intro 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
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
x : F
⊢ x ∈ segment ℝ y1 y2 ↔ (Homeomorph.refl F) x ∈ segment ℝ y2 y1
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
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
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
x : F
⊢ x ∈ segment ℝ y1 y2 ↔ (Homeomorph.refl F) x ∈ segment ℝ y2 y1
Tactic:
rw [segment_symm ℝ y2 y1]
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
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
x : F
⊢ x ∈ segment ℝ y1 y2 ↔ (Homeomorph.refl F) x ∈ segment ℝ y1 y2
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
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
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
x : F
⊢ x ∈ segment ℝ y1 y2 ↔ (Homeomorph.refl F) x ∈ segment ℝ y1 y2
Tactic:
simp only [Homeomorph.refl_apply, id_eq]
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
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
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 }
z : F
hz : z ∈ segment ℝ y1 y2
⊢ { val := z, property := hz } ∈ J2 ↔ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
Tactic:
simp [J2, J, φ, segment_symm ℝ y2 y1, hz]
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case mk
β : 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
z : F
hz : z ∈ segment ℝ y1 y2
hz1 : ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
hz2 : ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
hz_mem_Y : z ∈ Y
⊢ Disjoint (ERealSion.C X f t ↑{ val := z, property := hz_mem_Y })
    (ERealSion.C X f t ↑{ val := z, property := hz_mem_Y })
Tactic:
exact Set.disjoint_of_subset hz1 hz2 (disjoint_C X Y f a t' ⟨y1, hy1⟩ ⟨y2, hy2⟩ ha' ht')
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case h.mp.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 : J1 ∩ J2 = ∅
z : F
hz : z ∈ segment ℝ ↑{ val := y1, property := hy1 } ↑{ val := y2, property := hy2 }
left✝ : { val := z, property := hz } ∈ J1 ∪ J2
⊢ ↑{ val := z, property := hz } ∈ segment ℝ y1 y2
Tactic:
exact hz
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case h.inl.h
β : 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 = ∅
z : F
hz : z ∈ segment ℝ y1 y2
hz_mem_Y : z ∈ Y
h1 : ERealSion.C X f t' ↑{ val := z, property := hz } ⊆ ERealSion.C X f t' ↑{ val := y1, property := hy1 }
⊢ ERealSion.C X f t z ⊆ ERealSion.C X f t' y1
Tactic:
exact subset_trans (monotone_C X Y f t t' ⟨z, hz_mem_Y⟩ htt'.le) h1
Proof state after:
no goals
Theorem: ERealSion.exists_lt_iInf_of_lt_iInf_of_sup
Proof state before:
case h.inr.h
β : 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 = ∅
z : F
hz : z ∈ segment ℝ y1 y2
hz_mem_Y : z ∈ Y
h2 : ERealSion.C X f t' ↑{ val := z, property := hz } ⊆ ERealSion.C X f t' ↑{ val := y2, property := hy2 }
⊢ ERealSion.C X f t z ⊆ ERealSion.C X f t' y2
Tactic:
exact subset_trans (monotone_C X Y f t t' ⟨z, hz_mem_Y⟩ htt'.le) h2
Proof state after:
no goals
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
⊢ ERealSion.C X f t y2 ⊆ ERealSion.C X f t' y2
Tactic:
apply monotone_C X Y f t t' ⟨y2, hy2⟩ htt'.le
Proof state after:
no goals