ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>upperBounds {a} = Set.Ici a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>lowerBounds {a} = Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddAbove (Set.Icc a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddBelow (Set.Icc a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddAbove (Set.Ico a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddBelow (Set.Ico a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddAbove (Set.Ioc a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddBelow (Set.Ioc a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddAbove (Set.Ioo a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<GOAL>BddBelow (Set.Ioo a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>IsGreatest (Set.Icc a b) b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>IsLUB (Set.Icc a b) b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>upperBounds (Set.Icc a b) = Set.Ici b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>IsLeast (Set.Icc a b) a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>IsGLB (Set.Icc a b) a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>lowerBounds (Set.Icc a b) = Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>IsGreatest (Set.Ioc a b) b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>IsLUB (Set.Ioc a b) b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>upperBounds (Set.Ioc a b) = Set.Ici b
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>IsLeast (Set.Ico a b) a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>IsGLB (Set.Ico a b) a
<VAR>α : Type u<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>lowerBounds (Set.Ico a b) = Set.Iic a
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>h : a < b<GOAL>IsGLB (Set.Ioo a b) a
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>lowerBounds (Set.Ioo a b) = Set.Iic a
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>IsGLB (Set.Ioc a b) a
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>lowerBounds (Set.Ioc a b) = Set.Iic a
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>IsLUB (Set.Ioo a b) b
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>upperBounds (Set.Ioo a b) = Set.Ici b
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>IsLUB (Set.Ico a b) b
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>DenselyOrdered γ<VAR>a b : γ<VAR>hab : a < b<GOAL>upperBounds (Set.Ico a b) = Set.Ici b
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddBelow s ↔ ∃ a, s ⊆ Set.Ici a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddAbove s ↔ ∃ a, s ⊆ Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.Icc a b
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsGreatest Set.univ a ↔ IsTop a
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<GOAL>IsGreatest Set.univ ⊤
<VAR>γ : Type w<VAR>PartialOrder γ<VAR>OrderTop γ<GOAL>upperBounds Set.univ = {⊤}
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<GOAL>IsLUB Set.univ ⊤
<VAR>γ : Type w<VAR>PartialOrder γ<VAR>OrderBot γ<GOAL>lowerBounds Set.univ = {⊥}
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsLeast Set.univ a ↔ IsBot a
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<GOAL>IsLeast Set.univ ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<GOAL>IsGLB Set.univ ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>NoMaxOrder α<GOAL>upperBounds Set.univ = ∅
<VAR>α : Type u<VAR>Preorder α<VAR>NoMinOrder α<GOAL>lowerBounds Set.univ = ∅
<VAR>α : Type u<VAR>Preorder α<VAR>NoMaxOrder α<GOAL>¬BddAbove Set.univ
<VAR>α : Type u<VAR>Preorder α<VAR>NoMinOrder α<GOAL>¬BddBelow Set.univ
<VAR>α : Type u<VAR>Preorder α<GOAL>upperBounds ∅ = Set.univ
<VAR>α : Type u<VAR>Preorder α<GOAL>lowerBounds ∅ = Set.univ
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<GOAL>BddAbove ∅
<VAR>α : Type u<VAR>Preorder α<VAR>Nonempty α<GOAL>BddBelow ∅
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsGLB ∅ a ↔ IsTop a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsLUB ∅ a ↔ IsBot a
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<GOAL>IsGLB ∅ ⊤
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<GOAL>IsLUB ∅ ⊥
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>NoMinOrder α<VAR>hs : IsLUB s a<GOAL>s.Nonempty
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>NoMaxOrder α<VAR>hs : IsGLB s a<GOAL>s.Nonempty
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>ha : Nonempty α<VAR>h : ¬BddAbove s<GOAL>s.Nonempty
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>Nonempty α<VAR>h : ¬BddBelow s<GOAL>s.Nonempty
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>a : α<GOAL>BddAbove (insert a s) ↔ BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>a : α<GOAL>BddAbove s → BddAbove (insert a s)
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>s : Set α<VAR>a : α<GOAL>BddBelow (insert a s) ↔ BddBelow s
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>s : Set α<VAR>a : α<GOAL>BddBelow s → BddBelow (insert a s)
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>a : γ<VAR>b : γ<VAR>s : Set γ<VAR>hs : IsLUB s b<GOAL>IsLUB (insert a s) (a ⊔ b)
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>a : γ<VAR>b : γ<VAR>s : Set γ<VAR>hs : IsGLB s b<GOAL>IsGLB (insert a s) (a ⊓ b)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>a : γ<VAR>b : γ<VAR>s : Set γ<VAR>hs : IsGreatest s b<GOAL>IsGreatest (insert a s) (max a b)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>a : γ<VAR>b : γ<VAR>s : Set γ<VAR>hs : IsLeast s b<GOAL>IsLeast (insert a s) (min a b)
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>s : Set α<GOAL>upperBounds (insert a s) = Set.Ici a ∩ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>s : Set α<GOAL>lowerBounds (insert a s) = Set.Iic a ∩ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<VAR>s : Set α<GOAL>BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<VAR>s : Set α<GOAL>BddBelow s
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>a b : γ<GOAL>IsLUB {a, b} (a ⊔ b)
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>a b : γ<GOAL>IsGLB {a, b} (a ⊓ b)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>a b : γ<GOAL>IsLeast {a, b} (min a b)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>a b : γ<GOAL>IsGreatest {a, b} (max a b)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>IsLUB (lowerBounds s) a ↔ IsGLB s a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>IsGLB (upperBounds s) a ↔ IsLUB s a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ upperBounds s<GOAL>s.Nonempty → a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>ha : IsGLB s a<VAR>hb : IsLUB s b<VAR>hs : s.Nonempty<GOAL>a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>ha : IsLUB s a<GOAL>a < b ↔ ∃ c ∈ upperBounds s, c < b
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>ha : IsGLB s a<GOAL>b < a ↔ ∃ c ∈ lowerBounds s, b < c
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b x y : α<VAR>ha : IsGLB s a<VAR>hb : IsLUB s b<VAR>hab : b ≤ a<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x ≤ y
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsLeast s a<VAR>Hb : IsLeast s b<GOAL>a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsLeast s a<GOAL>IsLeast s b ↔ a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsGreatest s a<VAR>Hb : IsGreatest s b<GOAL>a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsGreatest s a<GOAL>IsGreatest s b ↔ a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsLUB s a<VAR>Hb : IsLUB s b<GOAL>a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsGLB s a<VAR>Hb : IsGLB s b<GOAL>a = b
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsGLB s a<VAR>Hb : IsLUB s b<VAR>hab : b ≤ a<GOAL>s.Subsingleton
<VAR>α : Type u<VAR>PartialOrder α<VAR>s : Set α<VAR>a b : α<VAR>Ha : IsGLB s a<VAR>Hb : IsLUB s b<VAR>x y : α<VAR>Hx : x ∈ s<VAR>Hy : y ∈ s<VAR>Hxy : x ≠ y<GOAL>a < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsLUB s a<GOAL>b < a ↔ ∃ c ∈ s, b < c
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsGLB s a<GOAL>a < b ↔ ∃ c ∈ s, c < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsLUB s a<VAR>hb : b < a<GOAL>∃ c ∈ s, b < c ∧ c ≤ a
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsLUB s a<VAR>h' : a ∉ s<VAR>hb : b < a<GOAL>∃ c ∈ s, b < c ∧ c < a
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsGLB s a<VAR>hb : a < b<GOAL>∃ c ∈ s, a ≤ c ∧ c < b
<VAR>α : Type u<VAR>LinearOrder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsGLB s a<VAR>h' : a ∉ s<VAR>hb : a < b<GOAL>∃ c ∈ s, a < c ∧ c < b
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<VAR>Has : a ∈ upperBounds s<VAR>Hat : a ∈ t<GOAL>f a ∈ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : MonotoneOn f t<GOAL>a ∈ upperBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<VAR>Has : a ∈ lowerBounds s<VAR>Hat : a ∈ t<GOAL>f a ∈ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : MonotoneOn f t<GOAL>a ∈ lowerBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<GOAL>f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<GOAL>f '' (lowerBounds s ∩ t) ⊆ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<GOAL>(upperBounds s ∩ t).Nonempty → BddAbove (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<GOAL>(lowerBounds s ∩ t).Nonempty → BddBelow (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : MonotoneOn f t<VAR>Ha : IsLeast t a<GOAL>IsLeast (f '' t) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : MonotoneOn f t<VAR>Ha : IsGreatest t a<GOAL>IsGreatest (f '' t) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>Hf : AntitoneOn f t<VAR>Hst : s ⊆ t<VAR>Has : a ∈ lowerBounds s<GOAL>a ∈ t → f a ∈ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : AntitoneOn f t<GOAL>a ∈ lowerBounds t → a ∈ t → f a ∈ upperBounds (f '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>Hf : AntitoneOn f t<VAR>Hst : s ⊆ t<GOAL>a ∈ upperBounds s → a ∈ t → f a ∈ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : AntitoneOn f t<GOAL>a ∈ upperBounds t → a ∈ t → f a ∈ lowerBounds (f '' t)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : AntitoneOn f t<VAR>Hst : s ⊆ t<GOAL>f '' (lowerBounds s ∩ t) ⊆ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : AntitoneOn f t<VAR>Hst : s ⊆ t<GOAL>f '' (upperBounds s ∩ t) ⊆ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : AntitoneOn f t<VAR>Hst : s ⊆ t<GOAL>(upperBounds s ∩ t).Nonempty → BddBelow (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>Hf : AntitoneOn f t<VAR>Hst : s ⊆ t<GOAL>(lowerBounds s ∩ t).Nonempty → BddAbove (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : AntitoneOn f t<GOAL>IsGreatest t a → IsLeast (f '' t) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>t : Set α<VAR>a : α<VAR>Hf : AntitoneOn f t<GOAL>IsLeast t a → IsGreatest (f '' t) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>a : α<VAR>s : Set α<VAR>Ha : a ∈ upperBounds s<GOAL>f a ∈ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>a : α<VAR>s : Set α<VAR>Ha : a ∈ lowerBounds s<GOAL>f a ∈ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>Hf : Monotone f<GOAL>f '' upperBounds s ⊆ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>s : Set α<GOAL>f '' lowerBounds s ⊆ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>s : Set α<GOAL>BddAbove s → BddAbove (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>s : Set α<GOAL>BddBelow s → BddBelow (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>a : α<VAR>s : Set α<VAR>Ha : IsLeast s a<GOAL>IsLeast (f '' s) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>Hf : Monotone f<VAR>a : α<VAR>s : Set α<VAR>Ha : IsGreatest s a<GOAL>IsGreatest (f '' s) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>a : α<VAR>s : Set α<GOAL>a ∈ lowerBounds s → f a ∈ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>a : α<VAR>s : Set α<GOAL>a ∈ upperBounds s → f a ∈ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>s : Set α<GOAL>f '' lowerBounds s ⊆ upperBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>s : Set α<GOAL>f '' upperBounds s ⊆ lowerBounds (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>s : Set α<GOAL>BddAbove s → BddBelow (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>s : Set α<GOAL>BddBelow s → BddAbove (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>a : α<VAR>s : Set α<GOAL>IsGreatest s a → IsLeast (f '' s) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Antitone f<VAR>a : α<VAR>s : Set α<GOAL>IsLeast s a → IsGreatest (f '' s) (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : a ∈ upperBounds s<VAR>hb : b ∈ upperBounds t<GOAL>f a b ∈ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ lowerBounds t<GOAL>f a b ∈ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>Set.image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>BddBelow s → BddBelow t → BddBelow (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : IsGreatest s a<VAR>hb : IsGreatest t b<GOAL>IsGreatest (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : IsLeast s a<VAR>hb : IsLeast t b<GOAL>IsLeast (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : a ∈ upperBounds s<VAR>hb : b ∈ lowerBounds t<GOAL>f a b ∈ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ upperBounds t<GOAL>f a b ∈ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>Set.image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>Set.image2 f (lowerBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>BddBelow s → BddAbove t → BddBelow (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : IsGreatest s a<VAR>hb : IsLeast t b<GOAL>IsGreatest (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Monotone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : IsLeast s a<VAR>hb : IsGreatest t b<GOAL>IsLeast (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ lowerBounds t<GOAL>f a b ∈ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : a ∈ upperBounds s<VAR>hb : b ∈ upperBounds t<GOAL>f a b ∈ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>Set.image2 f (lowerBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>Set.image2 f (upperBounds s) (upperBounds t) ⊆ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>BddBelow s → BddBelow t → BddAbove (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<GOAL>BddAbove s → BddAbove t → BddBelow (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : IsLeast s a<VAR>hb : IsLeast t b<GOAL>IsGreatest (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>ha : IsGreatest s a<VAR>hb : IsGreatest t b<GOAL>IsLeast (Set.image2 f s t) (f a b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : a ∈ lowerBounds s<VAR>hb : b ∈ upperBounds t<GOAL>f a b ∈ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>ha : a ∈ upperBounds s<VAR>hb : b ∈ lowerBounds t<GOAL>f a b ∈ lowerBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>Set.image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h₀ : ∀ (b : β), Antitone (Function.swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<GOAL>Set.image2 f (upperBounds s) (lowerBounds t) ⊆ lowerBounds (Set.image2 f s t)