ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 i j : ι<VAR>h_le : toZ i0 i ≤ toZ i0 j<GOAL>i ≤ j
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 i j : ι<VAR>h_le : i ≤ j<GOAL>toZ i0 i ≤ toZ i0 j
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>i j : ι<GOAL>toZ i0 i ≤ toZ i0 j ↔ i ≤ j
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>NoMaxOrder ι<VAR>n : ℕ<GOAL>toZ i0 (Order.succ^[n] i0) = ↑n
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<VAR>NoMinOrder ι<VAR>n : ℕ<GOAL>toZ i0 (Order.pred^[n] i0) = -↑n
<VAR>ι : Type u_1<VAR>LinearOrder ι<VAR>SuccOrder ι<VAR>IsSuccArchimedean ι<VAR>PredOrder ι<VAR>i0 : ι<GOAL>Function.Injective (toZ i0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x : α<GOAL>⇑e ⁻¹' Set.Ici (e x) = Set.Ici x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x : α<GOAL>⇑e ⁻¹' Set.Iic (e x) = Set.Iic x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x : α<GOAL>⇑e ⁻¹' Set.Ioi (e x) = Set.Ioi x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x : α<GOAL>⇑e ⁻¹' Set.Iio (e x) = Set.Iio x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Set.Icc (e x) (e y) = Set.Icc x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Set.Ico (e x) (e y) = Set.Ico x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Set.Ioc (e x) (e y) = Set.Ioc x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Set.Ioo (e x) (e y) = Set.Ioo x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Lattice β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Set.uIcc (e x) (e y) = Set.uIcc x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>LinearOrder β<VAR>e : α ↪o β<VAR>x y : α<GOAL>⇑e ⁻¹' Ι (e x) (e y) = Ι x y
<VAR>α : Type v<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Disjoint (Set.Iic a) (Set.Ioi b)
<VAR>α : Type v<VAR>Preorder α<VAR>a b : α<VAR>h : a ≤ b<GOAL>Disjoint (Set.Iio a) (Set.Ici b)
<VAR>α : Type v<VAR>Preorder α<VAR>a b c : α<VAR>h : a ≤ b<GOAL>Disjoint (Set.Iic a) (Set.Ioc b c)
<VAR>α : Type v<VAR>Preorder α<VAR>a b c : α<GOAL>Disjoint (Set.Ioc a b) (Set.Ioc b c)
<VAR>α : Type v<VAR>Preorder α<VAR>a b c : α<GOAL>Disjoint (Set.Ico a b) (Set.Ico b c)
<VAR>α : Type v<VAR>Preorder α<VAR>a b : α<GOAL>Disjoint (Set.Ici a) (Set.Iic b) ↔ ¬a ≤ b
<VAR>α : Type v<VAR>Preorder α<VAR>a b : α<GOAL>Disjoint (Set.Iic a) (Set.Ici b) ↔ ¬b ≤ a
<VAR>α : Type v<VAR>Preorder α<VAR>a b c : α<VAR>h : b ≤ c<GOAL>Disjoint (Set.Ioc a b) (Set.Ioi c)
<VAR>α : Type v<VAR>Preorder α<VAR>a b : α<GOAL>Disjoint (Set.Ioc a b) (Set.Ioi b)
<VAR>α : Type v<VAR>Preorder α<GOAL>⋃ a, Set.Iic a = Set.univ
<VAR>α : Type v<VAR>Preorder α<GOAL>⋃ a, Set.Ici a = Set.univ
<VAR>α : Type v<VAR>Preorder α<VAR>a : α<GOAL>⋃ b, Set.Icc a b = Set.Ici a
<VAR>α : Type v<VAR>Preorder α<VAR>a : α<GOAL>⋃ b, Set.Ioc a b = Set.Ioi a
<VAR>α : Type v<VAR>Preorder α<VAR>b : α<GOAL>⋃ a, Set.Icc a b = Set.Iic b
<VAR>α : Type v<VAR>Preorder α<VAR>b : α<GOAL>⋃ a, Set.Ico a b = Set.Iio b
<VAR>α : Type v<VAR>Preorder α<VAR>NoMaxOrder α<GOAL>⋃ a, Set.Iio a = Set.univ
<VAR>α : Type v<VAR>Preorder α<VAR>NoMinOrder α<GOAL>⋃ a, Set.Ioi a = Set.univ
<VAR>α : Type v<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>⋃ b, Set.Ico a b = Set.Ici a
<VAR>α : Type v<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>⋃ b, Set.Ioo a b = Set.Ioi a
<VAR>α : Type v<VAR>Preorder α<VAR>NoMinOrder α<VAR>b : α<GOAL>⋃ a, Set.Ioc a b = Set.Iic b
<VAR>α : Type v<VAR>Preorder α<VAR>NoMinOrder α<VAR>b : α<GOAL>⋃ a, Set.Ioo a b = Set.Iio b
<VAR>α : Type v<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Disjoint (Set.Ico a₁ a₂) (Set.Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>α : Type v<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<GOAL>Disjoint (Set.Ioc a₁ a₂) (Set.Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>α : Type v<VAR>LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>DenselyOrdered α<GOAL>Disjoint (Set.Ioo a₁ a₂) (Set.Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>α : Type v<VAR>LinearOrder α<VAR>x₁ x₂ y₁ y₂ : α<VAR>h : Disjoint (Set.Ico x₁ x₂) (Set.Ico y₁ y₂)<VAR>hx : x₁ < x₂<VAR>h2 : x₂ ∈ Set.Ico y₁ y₂<GOAL>y₁ = x₂
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>f : ι → α<VAR>a : α<GOAL>⋃ i, Set.Ico (f i) a = Set.Iio a ↔ ∀ x < a, ∃ i, f i ≤ x
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>f : ι → α<VAR>a : α<GOAL>⋃ i, Set.Ioc a (f i) = Set.Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<GOAL>⋃ i, ⋃ (hi : p i), Set.Ico (f i hi) a = Set.Iio a ↔ ∀ x < a, ∃ i, ∃ (hi : p i), f i hi ≤ x
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<GOAL>⋃ i, ⋃ (hi : p i), Set.Ioc a (f i hi) = Set.Ioi a ↔ ∀ (x : α), a < x → ∃ i, ∃ (hi : p i), x ≤ f i hi
<VAR>α : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGLB s a<GOAL>⋃ x ∈ s, Set.Ioi x = Set.Ioi a
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>a : α<VAR>f : ι → α<VAR>h : IsGLB (Set.range f) a<GOAL>⋃ x, Set.Ioi (f x) = Set.Ioi a
<VAR>α : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLUB s a<GOAL>⋃ x ∈ s, Set.Iio x = Set.Iio a
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>a : α<VAR>f : ι → α<VAR>h : IsLUB (Set.range f) a<GOAL>⋃ x, Set.Iio (f x) = Set.Iio a
<VAR>α : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>a_glb : IsGLB s a<VAR>a_not_mem : a ∉ s<GOAL>⋃ x ∈ s, Set.Ici x = Set.Ioi a
<VAR>α : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>a_glb : IsGLB s a<VAR>a_mem : a ∈ s<GOAL>⋃ x ∈ s, Set.Ici x = Set.Ici a
<VAR>α : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>a_lub : IsLUB s a<VAR>a_not_mem : a ∉ s<GOAL>⋃ x ∈ s, Set.Iic x = Set.Iio a
<VAR>α : Type v<VAR>LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>a_lub : IsLUB s a<VAR>a_mem : a ∈ s<GOAL>⋃ x ∈ s, Set.Iic x = Set.Iic a
<VAR>ι : Sort u<VAR>R : Type u_1<VAR>CompleteLinearOrder R<VAR>f : ι → R<VAR>no_least_elem : ⨅ i, f i ∉ Set.range f<GOAL>⋃ i, Set.Ici (f i) = Set.Ioi (⨅ i, f i)
<VAR>ι : Sort u<VAR>R : Type u_1<VAR>CompleteLinearOrder R<VAR>f : ι → R<VAR>no_greatest_elem : ⨆ i, f i ∉ Set.range f<GOAL>⋃ i, Set.Iic (f i) = Set.Iio (⨆ i, f i)
<VAR>ι : Sort u<VAR>R : Type u_1<VAR>CompleteLinearOrder R<VAR>f : ι → R<VAR>has_least_elem : ⨅ i, f i ∈ Set.range f<GOAL>⋃ i, Set.Ici (f i) = Set.Ici (⨅ i, f i)
<VAR>ι : Sort u<VAR>R : Type u_1<VAR>CompleteLinearOrder R<VAR>f : ι → R<VAR>has_greatest_elem : ⨆ i, f i ∈ Set.range f<GOAL>⋃ i, Set.Iic (f i) = Set.Iic (⨆ i, f i)
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>f : ι → α<GOAL>⋃ i, Set.Iio (f i) = Set.univ ↔ ¬BddAbove (Set.range f)
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>f : ι → α<VAR>hf : ¬BddAbove (Set.range f)<GOAL>⋃ i, Set.Iic (f i) = Set.univ
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>f : ι → α<GOAL>⋂ i, Set.Iic (f i) = ∅ ↔ ¬BddBelow (Set.range f)
<VAR>ι : Sort u<VAR>α : Type v<VAR>LinearOrder α<VAR>f : ι → α<VAR>hf : ¬BddBelow (Set.range f)<GOAL>⋂ i, Set.Iio (f i) = ∅
<VAR>α : Type u_1<GOAL>WithTop.some ⁻¹' {⊤} = ∅
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Set.range WithTop.some = Set.Iio ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some ⁻¹' Set.Ici ↑a = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some ⁻¹' Set.Iio ↑a = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some ⁻¹' Set.Iic ↑a = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<GOAL>WithTop.some ⁻¹' Set.Iio ⊤ = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some ⁻¹' Set.Ico ↑a ⊤ = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some ⁻¹' Set.Ioo ↑a ⊤ = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some '' Set.Ioi a = Set.Ioo ↑a ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some '' Set.Ici a = Set.Ico ↑a ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some '' Set.Iio a = Set.Iio ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithTop.some '' Set.Iic a = Set.Iic ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some '' Set.Icc a b = Set.Icc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some '' Set.Ico a b = Set.Ico ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some '' Set.Ioc a b = Set.Ioc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithTop.some '' Set.Ioo a b = Set.Ioo ↑a ↑b
<VAR>α : Type u_1<GOAL>WithBot.some ⁻¹' {⊥} = ∅
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Set.range WithBot.some = Set.Ioi ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some ⁻¹' Set.Ioi ↑a = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some ⁻¹' Set.Ici ↑a = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some ⁻¹' Set.Iio ↑a = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some ⁻¹' Set.Iic ↑a = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
<VAR>α : Type u_1<VAR>Preorder α<GOAL>WithBot.some ⁻¹' Set.Ioi ⊥ = Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some ⁻¹' Set.Ioc ⊥ ↑a = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some ⁻¹' Set.Ioo ⊥ ↑a = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some '' Set.Iio a = Set.Ioo ⊥ ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some '' Set.Iic a = Set.Ioc ⊥ ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some '' Set.Ioi a = Set.Ioi ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>WithBot.some '' Set.Ici a = Set.Ici ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some '' Set.Icc a b = Set.Icc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some '' Set.Ioc a b = Set.Ioc ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some '' Set.Ico a b = Set.Ico ↑a ↑b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>WithBot.some '' Set.Ioo a b = Set.Ioo ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>b : β<GOAL>⇑e ⁻¹' Set.Iic b = Set.Iic (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>b : β<GOAL>⇑e ⁻¹' Set.Ici b = Set.Ici (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>b : β<GOAL>⇑e ⁻¹' Set.Iio b = Set.Iio (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>b : β<GOAL>⇑e ⁻¹' Set.Ioi b = Set.Ioi (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Set.Icc a b = Set.Icc (e.symm a) (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Set.Ico a b = Set.Ico (e.symm a) (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Set.Ioc a b = Set.Ioc (e.symm a) (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : β<GOAL>⇑e ⁻¹' Set.Ioo a b = Set.Ioo (e.symm a) (e.symm b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a : α<GOAL>⇑e '' Set.Iic a = Set.Iic (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a : α<GOAL>⇑e '' Set.Ici a = Set.Ici (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a : α<GOAL>⇑e '' Set.Iio a = Set.Iio (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a : α<GOAL>⇑e '' Set.Ioi a = Set.Ioi (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Set.Ioo a b = Set.Ioo (e a) (e b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Set.Ioc a b = Set.Ioc (e a) (e b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Set.Ico a b = Set.Ico (e a) (e b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Set.Icc a b = Set.Icc (e a) (e b)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ upperBounds s ↔ ∀ x ∈ s, x ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ lowerBounds s ↔ ∀ x ∈ s, a ≤ x
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ upperBounds s ↔ s ⊆ Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ lowerBounds s ↔ s ⊆ Set.Ici a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddAbove s ↔ ∃ x, ∀ y ∈ s, y ≤ x
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddBelow s ↔ ∃ x, ∀ y ∈ s, x ≤ y
<VAR>α : Type u<VAR>Preorder α<VAR>OrderBot α<VAR>s : Set α<GOAL>⊥ ∈ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>OrderTop α<VAR>s : Set α<GOAL>⊤ ∈ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>OrderBot α<GOAL>IsLeast s ⊥ ↔ ⊥ ∈ s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>OrderTop α<GOAL>IsGreatest s ⊤ ↔ ⊤ ∈ s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, ¬y ≤ x
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, ¬x ≤ y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>¬BddAbove s ↔ ∀ (x : α), ∃ y ∈ s, x < y
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Set α<GOAL>¬BddBelow s ↔ ∀ (x : α), ∃ y ∈ s, y < x
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddBelow (⇑OrderDual.ofDual ⁻¹' s) ↔ BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>BddAbove (⇑OrderDual.ofDual ⁻¹' s) ↔ BddBelow s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set αᵒᵈ<GOAL>BddBelow (⇑OrderDual.toDual ⁻¹' s) ↔ BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set αᵒᵈ<GOAL>BddAbove (⇑OrderDual.toDual ⁻¹' s) ↔ BddBelow s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>h : BddAbove s<GOAL>BddBelow (⇑OrderDual.ofDual ⁻¹' s)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>h : BddBelow s<GOAL>BddAbove (⇑OrderDual.ofDual ⁻¹' s)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLeast s a<GOAL>IsGreatest (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGreatest s a<GOAL>IsLeast (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLUB s a<GOAL>IsGLB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGLB s a<GOAL>IsLUB (⇑OrderDual.ofDual ⁻¹' s) (OrderDual.toDual a)
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>hst : s ⊆ t<GOAL>upperBounds t ⊆ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>hst : s ⊆ t<GOAL>lowerBounds t ⊆ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>a ∈ upperBounds s → b ∈ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>b ∈ lowerBounds s → a ∈ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>a b : α<VAR>hab : a ≤ b<GOAL>a ∈ upperBounds t → b ∈ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>a b : α<VAR>hab : a ≤ b<GOAL>b ∈ lowerBounds t → a ∈ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>BddAbove t → BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>BddBelow t → BddBelow s
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>s t p : Set α<VAR>hs : IsLUB s a<VAR>hp : IsLUB p a<VAR>hst : s ⊆ t<VAR>htp : t ⊆ p<GOAL>IsLUB t a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>s t p : Set α<VAR>hs : IsGLB s a<VAR>hp : IsGLB p a<VAR>hst : s ⊆ t<VAR>htp : t ⊆ p<GOAL>IsGLB t a
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>a b : α<VAR>ha : IsLeast s a<VAR>hb : IsLeast t b<VAR>hst : s ⊆ t<GOAL>b ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>a b : α<VAR>ha : IsGreatest s a<VAR>hb : IsGreatest t b<VAR>hst : s ⊆ t<GOAL>a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>a b : α<VAR>ha : IsLUB s a<VAR>hb : IsLUB t b<VAR>hst : s ⊆ t<GOAL>a ≤ b
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>a b : α<VAR>ha : IsGLB s a<VAR>hb : IsGLB t b<VAR>hst : s ⊆ t<GOAL>b ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>s ⊆ lowerBounds (upperBounds s)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<GOAL>s ⊆ upperBounds (lowerBounds s)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>BddAbove (lowerBounds s)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>BddBelow (upperBounds s)
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLeast s a<GOAL>IsGLB s a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGreatest s a<GOAL>IsLUB s a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLUB s a<GOAL>upperBounds s = Set.Ici a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGLB s a<GOAL>lowerBounds s = Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLeast s a<GOAL>lowerBounds s = Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGreatest s a<GOAL>upperBounds s = Set.Ici a
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsGreatest s a<GOAL>a < b ↔ ∀ x ∈ s, x < b
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsLeast s a<GOAL>b < a ↔ ∀ x ∈ s, b < x
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsLUB s a<GOAL>a ≤ b ↔ b ∈ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a b : α<VAR>h : IsGLB s a<GOAL>b ≤ a ↔ b ∈ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<GOAL>IsGLB s a ↔ ∀ (b : α), b ≤ a ↔ b ∈ lowerBounds s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLUB s a<GOAL>BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGLB s a<GOAL>BddBelow s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGreatest s a<GOAL>BddAbove s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLeast s a<GOAL>BddBelow s
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsLeast s a<GOAL>s.Nonempty
<VAR>α : Type u<VAR>Preorder α<VAR>s : Set α<VAR>a : α<VAR>h : IsGreatest s a<GOAL>s.Nonempty
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<GOAL>upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<GOAL>lowerBounds (s ∪ t) = lowerBounds s ∩ lowerBounds t
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<GOAL>upperBounds s ∪ upperBounds t ⊆ upperBounds (s ∩ t)
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<GOAL>lowerBounds s ∪ lowerBounds t ⊆ lowerBounds (s ∩ t)
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<VAR>s t : Set α<GOAL>IsLeast (s ∪ t) a ↔ IsLeast s a ∧ a ∈ lowerBounds t ∨ a ∈ lowerBounds s ∧ IsLeast t a
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>a : α<GOAL>IsGreatest (s ∪ t) a ↔ IsGreatest s a ∧ a ∈ upperBounds t ∨ a ∈ upperBounds s ∧ IsGreatest t a
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>h : BddAbove s<GOAL>BddAbove (s ∩ t)
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>h : BddAbove t<GOAL>BddAbove (s ∩ t)
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>h : BddBelow s<GOAL>BddBelow (s ∩ t)
<VAR>α : Type u<VAR>Preorder α<VAR>s t : Set α<VAR>h : BddBelow t<GOAL>BddBelow (s ∩ t)
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>BddAbove s → BddAbove t → BddAbove (s ∪ t)
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>BddAbove (s ∪ t) ↔ BddAbove s ∧ BddAbove t
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>s t : Set α<GOAL>BddBelow s → BddBelow t → BddBelow (s ∪ t)
<VAR>α : Type u<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≥ x_1<VAR>s t : Set α<GOAL>BddBelow (s ∪ t) ↔ BddBelow s ∧ BddBelow t
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>a b : γ<VAR>s t : Set γ<VAR>hs : IsLUB s a<VAR>ht : IsLUB t b<GOAL>IsLUB (s ∪ t) (a ⊔ b)
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>a₁ a₂ : γ<VAR>s t : Set γ<VAR>hs : IsGLB s a₁<VAR>ht : IsGLB t a₂<GOAL>IsGLB (s ∪ t) (a₁ ⊓ a₂)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>a b : γ<VAR>s t : Set γ<VAR>ha : IsLeast s a<VAR>hb : IsLeast t b<GOAL>IsLeast (s ∪ t) (min a b)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>a b : γ<VAR>s t : Set γ<VAR>ha : IsGreatest s a<VAR>hb : IsGreatest t b<GOAL>IsGreatest (s ∪ t) (max a b)
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>s : Set γ<VAR>a b : γ<VAR>ha : IsLUB s a<VAR>hb : b ∈ s<GOAL>IsLUB (s ∩ Set.Ici b) a
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>s : Set γ<VAR>a b : γ<VAR>ha : IsGLB s a<VAR>hb : b ∈ s<GOAL>IsGLB (s ∩ Set.Iic b) a
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>s : Set γ<VAR>x₀ : γ<GOAL>BddAbove s ↔ ∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>s : Set γ<VAR>x₀ : γ<GOAL>BddBelow s ↔ ∃ x ≤ x₀, ∀ y ∈ s, x ≤ y
<VAR>γ : Type w<VAR>SemilatticeSup γ<VAR>s : Set γ<VAR>hs : BddAbove s<VAR>x₀ : γ<GOAL>∃ x, x₀ ≤ x ∧ ∀ y ∈ s, y ≤ x
<VAR>γ : Type w<VAR>SemilatticeInf γ<VAR>s : Set γ<VAR>hs : BddBelow s<VAR>x₀ : γ<GOAL>∃ x ≤ x₀, ∀ y ∈ s, x ≤ y
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsLeast (Set.Ici a) a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsGreatest (Set.Iic a) a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsLUB (Set.Iic a) a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsGLB (Set.Ici a) a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>upperBounds (Set.Iic a) = Set.Ici a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>lowerBounds (Set.Ici a) = Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>BddAbove (Set.Iic a)
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>BddBelow (Set.Ici a)
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>BddAbove (Set.Iio a)
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>BddBelow (Set.Ioi a)
<VAR>α : Type u<VAR>Preorder α<VAR>b : α<VAR>a : α<VAR>hb : IsLUB (Set.Iio a) b<GOAL>b ≤ a
<VAR>α : Type u<VAR>Preorder α<VAR>b : α<VAR>a : α<VAR>hb : IsGLB (Set.Ioi a) b<GOAL>a ≤ b
<VAR>γ : Type w<VAR>PartialOrder γ<VAR>j : γ<VAR>i : γ<VAR>hj : IsLUB (Set.Iio i) j<GOAL>j = i ∨ Set.Iio i = Set.Iic j
<VAR>γ : Type w<VAR>PartialOrder γ<VAR>j : γ<VAR>i : γ<VAR>hj : IsGLB (Set.Ioi i) j<GOAL>j = i ∨ Set.Ioi i = Set.Ici j
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>i : γ<GOAL>∃ j, IsLUB (Set.Iio i) j
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>i : γ<GOAL>∃ j, IsGLB (Set.Ioi i) j
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>DenselyOrdered γ<VAR>a : γ<GOAL>IsLUB (Set.Iio a) a
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>DenselyOrdered γ<VAR>a : γ<GOAL>IsGLB (Set.Ioi a) a
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>DenselyOrdered γ<VAR>a : γ<GOAL>upperBounds (Set.Iio a) = Set.Ici a
<VAR>γ : Type w<VAR>LinearOrder γ<VAR>DenselyOrdered γ<VAR>a : γ<GOAL>lowerBounds (Set.Ioi a) = Set.Iic a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsGreatest {a} a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsLeast {a} a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsLUB {a} a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>IsGLB {a} a
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>BddAbove {a}
<VAR>α : Type u<VAR>Preorder α<VAR>a : α<GOAL>BddBelow {a}