internlm/Lean-Github huggingface dataset:
Theorem: Convex.quasiconvexOn_restrict
Proof state before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ f x ≤ b}
Tactic:
rw [Set.sep_of_subset hst]
Proof state after:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ b} ∩ t)
Theorem: Convex.quasiconvexOn_restrict
Proof state before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconvexOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ f x ≤ b} ∩ t)
Tactic:
exact Convex.inter (hf b) ht
Proof state after:
no goals
Theorem: Convex.quasiconcaveOn_restrict
Proof state before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
⊢ QuasiconcaveOn 𝕜 t f
Tactic:
intro b
Proof state after:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ b ≤ f x}
Theorem: Convex.quasiconcaveOn_restrict
Proof state before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 {x | x ∈ t ∧ b ≤ f x}
Tactic:
rw [Set.sep_of_subset hst]
Proof state after:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ b ≤ f x} ∩ t)
Theorem: Convex.quasiconcaveOn_restrict
Proof state before:
𝕜 : Type u_3
E : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : SMul 𝕜 E
β : Type u_2
inst✝ : Preorder β
s : Set E
f : E → β
t : Set E
hf : QuasiconcaveOn 𝕜 s f
hst : t ⊆ s
ht : Convex 𝕜 t
b : β
⊢ Convex 𝕜 ({x | x ∈ s ∧ b ≤ f x} ∩ t)
Tactic:
exact Convex.inter (hf b) ht
Proof state after:
no goals
Theorem: QuasiconcaveOn.isPreconnected_preimage
Proof state before:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected ((f ∘ fun x => ↑x) ⁻¹' Ici t)
Tactic:
rw [preimage_comp, ← inducing_subtype_val.isPreconnected_image, image_preimage_eq_inter_range,
  Subtype.range_coe, inter_comm]
Proof state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Ici t)
Theorem: QuasiconcaveOn.isPreconnected_preimage
Proof state before:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconcaveOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Ici t)
Tactic:
exact (hfc t).isPreconnected
Proof state after:
no goals
Theorem: QuasiconvexOn.isPreconnected_preimage
Proof state before:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconvexOn ℝ s f
⊢ IsPreconnected ((f ∘ fun x => ↑x) ⁻¹' Iic t)
Tactic:
rw [preimage_comp, ← inducing_subtype_val.isPreconnected_image, image_preimage_eq_inter_range,
  Subtype.range_coe, inter_comm]
Proof state after:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconvexOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Iic t)
Theorem: QuasiconvexOn.isPreconnected_preimage
Proof state before:
E : Type u_1
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousSMul ℝ E
β : Type u_2
inst✝ : Preorder β
f : E → β
s : Set E
t : β
hfc : QuasiconvexOn ℝ s f
⊢ IsPreconnected (s ∩ f ⁻¹' Iic t)
Tactic:
exact (hfc t).isPreconnected
Proof state after:
no goals
Theorem: iSup₂_iInf₂_le_iInf₂_iSup₂
Proof state before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ⨆ y ∈ Y, ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
rw [iSup₂_le_iff]
Proof state after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Theorem: iSup₂_iInf₂_le_iInf₂_iSup₂
Proof state before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
⊢ ∀ i ∈ Y, ⨅ x ∈ X, f x i ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
intro y hy
Proof state after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Theorem: iSup₂_iInf₂_le_iInf₂_iSup₂
Proof state before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
Tactic:
rw [le_iInf₂_iff]
Proof state after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y
Theorem: iSup₂_iInf₂_le_iInf₂_iSup₂
Proof state before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y
Tactic:
intro x hx
Proof state after:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f x y
Theorem: iSup₂_iInf₂_le_iInf₂_iSup₂
Proof state before:
E : Type u_3
F : Type u_2
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f x y
Tactic:
exact iInf₂_le_of_le x hx (le_iSup₂_of_le y hy (le_refl _))
Proof state after:
no goals
Theorem: isSaddlePointOn_iff
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
constructor
Proof state after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b → ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

case mpr
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b → IsSaddlePointOn X Y f a b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b → ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
intro h
Proof state after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
dsimp [IsSaddlePointOn] at h
Proof state after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
constructor
Proof state after:
case mp.left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b

case mp.right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b = f a b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y = f a b
Tactic:
apply le_antisymm
Proof state after:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b
Tactic:
simp only [iSup_le_iff]
Proof state after:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ Y, f a i ≤ f a b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ Y, f a i ≤ f a b
Tactic:
exact h a ha
Proof state after:
no goals
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Tactic:
apply le_iSup₂ b hb
Proof state after:
no goals
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b = f a b
Tactic:
apply le_antisymm
Proof state after:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b

case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨅ x ∈ X, f x b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b
Tactic:
apply iInf₂_le a ha
Proof state after:
no goals
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ f a b ≤ ⨅ x ∈ X, f x b
Tactic:
simp only [le_iInf_iff]
Proof state after:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ X, f a b ≤ f i b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
⊢ ∀ i ∈ X, f a b ≤ f i b
Tactic:
intro x hx
Proof state after:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b
Theorem: isSaddlePointOn_iff
Proof state before:
case mp.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ∀ x ∈ X, ∀ y ∈ Y, f a y ≤ f x b
x : E
hx : x ∈ X
⊢ f a b ≤ f x b
Tactic:
exact h x hx b hb
Proof state after:
no goals
Theorem: isSaddlePointOn_iff
Proof state before:
case mpr
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b → IsSaddlePointOn X Y f a b
Tactic:
rintro ⟨h, h'⟩
Proof state after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ IsSaddlePointOn X Y f a b
Theorem: isSaddlePointOn_iff
Proof state before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ IsSaddlePointOn X Y f a b
Tactic:
intro x hx y hy
Proof state after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b
Theorem: isSaddlePointOn_iff
Proof state before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f x b
Tactic:
suffices f a y ≤ f a b by
  apply le_trans this
  rw [← h']
  apply iInf₂_le x hx
Proof state after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f a b
Theorem: isSaddlePointOn_iff
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ f a y ≤ f x b
Tactic:
apply le_trans this
Proof state after:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ f a b ≤ f x b
Theorem: isSaddlePointOn_iff
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ f a b ≤ f x b
Tactic:
rw [← h']
Proof state after:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b
Theorem: isSaddlePointOn_iff
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
this : f a y ≤ f a b
⊢ ⨅ x ∈ X, f x b ≤ f x b
Tactic:
apply iInf₂_le x hx
Proof state after:
no goals
Theorem: isSaddlePointOn_iff
Proof state before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ f a b
Tactic:
rw [← h]
Proof state after:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ ⨆ y ∈ Y, f a y
Theorem: isSaddlePointOn_iff
Proof state before:
case mpr.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
⊢ f a y ≤ ⨆ y ∈ Y, f a y
Tactic:
apply le_iSup₂ y hy
Proof state after:
no goals
Theorem: isSaddlePointOn_iff'
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
Tactic:
rw [isSaddlePointOn_iff ha hb]
Proof state after:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
Theorem: isSaddlePointOn_iff'
Proof state before:
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b ↔ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
Tactic:
constructor
Proof state after:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b → ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b

case mpr
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b → ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Theorem: isSaddlePointOn_iff'
Proof state before:
case mp
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b → ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
Tactic:
rintro ⟨h, h'⟩
Proof state after:
case mp.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
Theorem: isSaddlePointOn_iff'
Proof state before:
case mp.intro
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
Tactic:
exact le_trans (le_of_eq h) (le_of_eq h'.symm)
Proof state after:
no goals
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b → ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
intro h
Proof state after:
case mpr
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
Tactic:
constructor
Proof state after:
case mpr.left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b

case mpr.right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.left
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y = f a b
Tactic:
apply le_antisymm
Proof state after:
case mpr.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b

case mpr.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨆ y ∈ Y, f a y ≤ f a b
Tactic:
apply le_trans h
Proof state after:
case mpr.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b
Tactic:
apply iInf₂_le a ha
Proof state after:
no goals
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.left.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨆ y ∈ Y, f a y
Tactic:
apply le_iSup₂ b hb
Proof state after:
no goals
Theorem: isSaddlePointOn_iff'
Proof state before:
case mpr.right
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b = f a b
Tactic:
apply le_antisymm
Proof state after:
case mpr.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ ⨅ x ∈ X, f x b ≤ f a b

case mpr.right.a
E : Type u_2
F : Type u_3
β : Type u_1
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y ≤ ⨅ x ∈ X, f x b
⊢ f a b ≤ ⨅ x ∈ X, f x b