ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>ht : IsAntichain r t<VAR>h : minimals r s ⊆ t<VAR>hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ minimals r s, r a b<GOAL>minimals r s = t
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<VAR>h : IsLeast s a<GOAL>a ∈ minimals (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Preorder α<VAR>h : IsGreatest s a<GOAL>a ∈ maximals (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>PartialOrder α<VAR>h : IsLeast s a<GOAL>minimals (fun x x_1 => x ≤ x_1) s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>PartialOrder α<VAR>h : IsGreatest s a<GOAL>maximals (fun x x_1 => x ≤ x_1) s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>PartialOrder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>minimals (fun x x_1 => x ≤ x_1) ↑(upperClosure s) = s
<VAR>α : Type u_1<VAR>s : Set α<VAR>PartialOrder α<VAR>hs : IsAntichain (fun x x_1 => x ≤ x_1) s<GOAL>maximals (fun x x_1 => x ≤ x_1) ↑(lowerClosure s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>a : α<VAR>ha : a ∈ minimals r x<GOAL>f a ∈ minimals s (f '' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>a : α<VAR>ha : a ∈ maximals r x<GOAL>f a ∈ maximals s (f '' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>a : α<VAR>ha : a ∈ x<GOAL>f a ∈ minimals s (f '' x) ↔ a ∈ minimals r x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>a : α<VAR>ha : a ∈ x<GOAL>f a ∈ maximals s (f '' x) ↔ a ∈ maximals r x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<GOAL>f '' minimals r x = minimals s (f '' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<GOAL>f '' maximals r x = maximals s (f '' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<GOAL>⇑f '' minimals r x = minimals s (⇑f '' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<GOAL>⇑f '' maximals r x = maximals s (⇑f '' x)
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<GOAL>Subtype.val '' minimals (fun x x_1 => x ≤ x_1) Set.univ = minimals (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<GOAL>Subtype.val '' maximals (fun x x_1 => x ≤ x_1) Set.univ = maximals (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>s : Set α<VAR>t : Set β<VAR>f : ↑s ≃o ↑t<VAR>x : α<VAR>hx : x ∈ minimals (fun x x_1 => x ≤ x_1) s<GOAL>↑(f ⟨x, ⋯⟩) ∈ minimals (fun x x_1 => x ≤ x_1) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LE α<VAR>LE β<VAR>s : Set α<VAR>t : Set β<VAR>f : ↑s ≃o ↑t<VAR>x : α<VAR>hx : x ∈ maximals (fun x x_1 => x ≤ x_1) s<GOAL>↑(f ⟨x, ⋯⟩) ∈ maximals (fun x x_1 => x ≤ x_1) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>y : Set β<GOAL>x ∩ f ⁻¹' minimals s (f '' x ∩ y) = minimals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>y : Set β<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>hy : y ⊆ f '' x<GOAL>x ∩ f ⁻¹' minimals s y = minimals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<VAR>y : Set β<GOAL>x ∩ ⇑f ⁻¹' minimals s (⇑f '' x ∩ y) = minimals r (x ∩ ⇑f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>f : r ↪r s<VAR>h : y ⊆ ⇑f '' x<GOAL>x ∩ ⇑f ⁻¹' minimals s y = minimals r (x ∩ ⇑f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>minimals r (⇑f ⁻¹' y) = ⇑f ⁻¹' minimals s (y ∩ Set.range ⇑f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<VAR>y : Set β<GOAL>minimals r (⇑f ⁻¹' y) = ⇑f ⁻¹' minimals s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ≃r s<VAR>y : Set β<GOAL>maximals r (⇑f ⁻¹' y) = ⇑f ⁻¹' maximals s y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>y : Set β<GOAL>x ∩ f ⁻¹' maximals s (f '' x ∩ y) = maximals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>hy : y ⊆ f '' x<GOAL>x ∩ f ⁻¹' maximals s y = maximals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<VAR>y : Set β<GOAL>x ∩ ⇑f ⁻¹' maximals s (⇑f '' x ∩ y) = maximals r (x ∩ ⇑f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>f : r ↪r s<VAR>h : y ⊆ ⇑f '' x<GOAL>x ∩ ⇑f ⁻¹' maximals s y = maximals r (x ∩ ⇑f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>maximals r (⇑f ⁻¹' y) = ⇑f ⁻¹' maximals s (y ∩ Set.range ⇑f)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>maximals (fun x x_1 => x ≤ x_1) (Set.Iic a) = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a : α<GOAL>minimals (fun x x_1 => x ≤ x_1) (Set.Ici a) = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>maximals (fun x x_1 => x ≤ x_1) (Set.Icc a b) = {b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a ≤ b<GOAL>minimals (fun x x_1 => x ≤ x_1) (Set.Icc a b) = {a}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a < b<GOAL>maximals (fun x x_1 => x ≤ x_1) (Set.Ioc a b) = {b}
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>hab : a < b<GOAL>minimals (fun x x_1 => x ≤ x_1) (Set.Ico a b) = {a}
<VAR>α : Type u_2<VAR>SemilatticeSup α<GOAL>SupClosed ∅
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>SupClosed {a}
<VAR>α : Type u_2<VAR>SemilatticeSup α<GOAL>SupClosed Set.univ
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<VAR>hs : SupClosed s<VAR>ht : SupClosed t<GOAL>SupClosed (s ∩ t)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, SupClosed s<GOAL>SupClosed (⋂₀ S)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>ι : Sort u_4<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), SupClosed (f i)<GOAL>SupClosed (⋂ i, f i)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>hs : SupClosed s<GOAL>DirectedOn (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>SupClosed s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>s : Set α<VAR>FunLike F β α<VAR>SupHomClass F β α<VAR>hs : SupClosed s<VAR>f : F<GOAL>SupClosed (⇑f ⁻¹' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>s : Set α<VAR>FunLike F α β<VAR>SupHomClass F α β<VAR>hs : SupClosed s<VAR>f : F<GOAL>SupClosed (⇑f '' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>FunLike F α β<VAR>SupHomClass F α β<VAR>f : F<GOAL>SupClosed (Set.range ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>s : Set α<VAR>t : Set β<VAR>hs : SupClosed s<VAR>ht : SupClosed t<GOAL>SupClosed (s ×ˢ t)
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>(i : ι) → SemilatticeSup (α i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>ht : ∀ i ∈ s, SupClosed (t i)<GOAL>SupClosed (s.pi t)
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>ι : Type u_4<VAR>f : ι → α<VAR>s : Set α<VAR>t : Finset ι<VAR>hs : SupClosed s<VAR>ht : t.Nonempty<GOAL>(∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>ι : Type u_4<VAR>f : ι → α<VAR>s : Set α<VAR>t : Finset ι<VAR>OrderBot α<VAR>hs : SupClosed s<VAR>ht : t.Nonempty<GOAL>(∀ i ∈ t, f i ∈ s) → t.sup f ∈ s
<VAR>α : Type u_2<VAR>SemilatticeInf α<GOAL>InfClosed ∅
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>InfClosed {a}
<VAR>α : Type u_2<VAR>SemilatticeInf α<GOAL>InfClosed Set.univ
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<VAR>hs : InfClosed s<VAR>ht : InfClosed t<GOAL>InfClosed (s ∩ t)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, InfClosed s<GOAL>InfClosed (⋂₀ S)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>ι : Sort u_4<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), InfClosed (f i)<GOAL>InfClosed (⋂ i, f i)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>hs : InfClosed s<GOAL>DirectedOn (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>InfClosed s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>s : Set α<VAR>FunLike F β α<VAR>InfHomClass F β α<VAR>hs : InfClosed s<VAR>f : F<GOAL>InfClosed (⇑f ⁻¹' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>s : Set α<VAR>FunLike F α β<VAR>InfHomClass F α β<VAR>hs : InfClosed s<VAR>f : F<GOAL>InfClosed (⇑f '' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>FunLike F α β<VAR>InfHomClass F α β<VAR>f : F<GOAL>InfClosed (Set.range ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>s : Set α<VAR>t : Set β<VAR>hs : InfClosed s<VAR>ht : InfClosed t<GOAL>InfClosed (s ×ˢ t)
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>(i : ι) → SemilatticeInf (α i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>ht : ∀ i ∈ s, InfClosed (t i)<GOAL>InfClosed (s.pi t)
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>ι : Type u_4<VAR>f : ι → α<VAR>s : Set α<VAR>t : Finset ι<VAR>hs : InfClosed s<VAR>ht : t.Nonempty<GOAL>(∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>ι : Type u_4<VAR>f : ι → α<VAR>s : Set α<VAR>t : Finset ι<VAR>OrderTop α<VAR>hs : InfClosed s<VAR>ht : t.Nonempty<GOAL>(∀ i ∈ t, f i ∈ s) → t.inf f ∈ s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<VAR>self : IsSublattice s<GOAL>InfClosed s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<VAR>self : IsSublattice s<GOAL>SupClosed s
<VAR>α : Type u_2<VAR>Lattice α<GOAL>IsSublattice ∅
<VAR>α : Type u_2<VAR>Lattice α<VAR>a : α<GOAL>IsSublattice {a}
<VAR>α : Type u_2<VAR>Lattice α<GOAL>IsSublattice Set.univ
<VAR>α : Type u_2<VAR>Lattice α<VAR>s t : Set α<VAR>hs : IsSublattice s<VAR>ht : IsSublattice t<GOAL>IsSublattice (s ∩ t)
<VAR>α : Type u_2<VAR>Lattice α<VAR>S : Set (Set α)<VAR>hS : ∀ s ∈ S, IsSublattice s<GOAL>IsSublattice (⋂₀ S)
<VAR>α : Type u_2<VAR>ι : Sort u_4<VAR>Lattice α<VAR>f : ι → Set α<VAR>hf : ∀ (i : ι), IsSublattice (f i)<GOAL>IsSublattice (⋂ i, f i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>s : Set α<VAR>FunLike F β α<VAR>LatticeHomClass F β α<VAR>hs : IsSublattice s<VAR>f : F<GOAL>IsSublattice (⇑f ⁻¹' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>s : Set α<VAR>FunLike F α β<VAR>LatticeHomClass F α β<VAR>hs : IsSublattice s<VAR>f : F<GOAL>IsSublattice (⇑f '' s)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>FunLike F α β<VAR>LatticeHomClass F α β<VAR>f : F<GOAL>IsSublattice (Set.range ⇑f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Lattice α<VAR>Lattice β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsSublattice s<VAR>ht : IsSublattice t<GOAL>IsSublattice (s ×ˢ t)
<VAR>ι : Type u_5<VAR>α : ι → Type u_6<VAR>(i : ι) → Lattice (α i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>ht : ∀ i ∈ s, IsSublattice (t i)<GOAL>IsSublattice (s.pi t)
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set αᵒᵈ<GOAL>SupClosed (⇑OrderDual.toDual ⁻¹' s) ↔ InfClosed s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set αᵒᵈ<GOAL>InfClosed (⇑OrderDual.toDual ⁻¹' s) ↔ SupClosed s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>SupClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ InfClosed s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>InfClosed (⇑OrderDual.ofDual ⁻¹' s) ↔ SupClosed s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set αᵒᵈ<GOAL>IsSublattice (⇑OrderDual.toDual ⁻¹' s) ↔ IsSublattice s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>IsSublattice (⇑OrderDual.ofDual ⁻¹' s) ↔ IsSublattice s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<GOAL>SupClosed s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<GOAL>InfClosed s
<VAR>α : Type u_2<VAR>LinearOrder α<VAR>s : Set α<GOAL>IsSublattice s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>supClosure.IsClosed s = SupClosed s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>s ⊆ supClosure s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>SupClosed (supClosure s)
<VAR>α : Type u_2<VAR>SemilatticeSup α<GOAL>Monotone ⇑supClosure
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>supClosure s = s ↔ SupClosed s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>supClosure (supClosure s) = supClosure s
<VAR>α : Type u_2<VAR>SemilatticeSup α<GOAL>supClosure ∅ = ∅
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>a : α<GOAL>supClosure {a} = {a}
<VAR>α : Type u_2<VAR>SemilatticeSup α<GOAL>supClosure Set.univ = Set.univ
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<GOAL>upperBounds (supClosure s) = upperBounds s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>a : α<GOAL>IsLUB (supClosure s) a ↔ IsLUB s a
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a ⊔ b ∈ supClosure s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>ht : t.Nonempty<VAR>f : ι → α<VAR>hf : ∀ i ∈ t, f i ∈ s<GOAL>t.sup' ht f ∈ supClosure s
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s t : Set α<GOAL>s ⊆ t → SupClosed t → supClosure s ⊆ t
<VAR>α : Type u_2<VAR>SemilatticeSup α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(supClosure s).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeSup α<VAR>SemilatticeSup β<VAR>s : Set α<VAR>t : Set β<GOAL>supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>infClosure.IsClosed s = InfClosed s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>s ⊆ infClosure s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>InfClosed (infClosure s)
<VAR>α : Type u_2<VAR>SemilatticeInf α<GOAL>Monotone ⇑infClosure
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>infClosure s = s ↔ InfClosed s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>infClosure (infClosure s) = infClosure s
<VAR>α : Type u_2<VAR>SemilatticeInf α<GOAL>infClosure ∅ = ∅
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>a : α<GOAL>infClosure {a} = {a}
<VAR>α : Type u_2<VAR>SemilatticeInf α<GOAL>infClosure Set.univ = Set.univ
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<GOAL>lowerBounds (infClosure s) = lowerBounds s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>a : α<GOAL>IsGLB (infClosure s) a ↔ IsGLB s a
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a ⊓ b ∈ infClosure s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>ι : Type u_4<VAR>t : Finset ι<VAR>ht : t.Nonempty<VAR>f : ι → α<VAR>hf : ∀ i ∈ t, f i ∈ s<GOAL>t.inf' ht f ∈ infClosure s
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s t : Set α<GOAL>s ⊆ t → InfClosed t → infClosure s ⊆ t
<VAR>α : Type u_2<VAR>SemilatticeInf α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(infClosure s).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SemilatticeInf α<VAR>SemilatticeInf β<VAR>s : Set α<VAR>t : Set β<GOAL>infClosure (s ×ˢ t) = infClosure s ×ˢ infClosure t
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>latticeClosure.IsClosed s = IsSublattice s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>s ⊆ latticeClosure s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>IsSublattice (latticeClosure s)
<VAR>α : Type u_2<VAR>Lattice α<VAR>s t : Set α<GOAL>s ⊆ t → IsSublattice t → latticeClosure s ⊆ t
<VAR>α : Type u_2<VAR>Lattice α<GOAL>Monotone ⇑latticeClosure
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>latticeClosure s = s ↔ IsSublattice s
<VAR>α : Type u_2<VAR>Lattice α<VAR>s : Set α<GOAL>latticeClosure (latticeClosure s) = latticeClosure s
<VAR>α : Type u_2<VAR>Lattice α<GOAL>latticeClosure ∅ = ∅
<VAR>α : Type u_2<VAR>Lattice α<VAR>a : α<GOAL>latticeClosure {a} = {a}
<VAR>α : Type u_2<VAR>Lattice α<GOAL>latticeClosure Set.univ = Set.univ
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s : Set α<VAR>hs : SupClosed s<GOAL>SupClosed (infClosure s)
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s : Set α<VAR>hs : InfClosed s<GOAL>InfClosed (supClosure s)
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s : Set α<GOAL>supClosure (infClosure s) = latticeClosure s
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s : Set α<GOAL>infClosure (supClosure s) = latticeClosure s
<VAR>α : Type u_2<VAR>DistribLattice α<VAR>s : Set α<VAR>hs : s.Finite<GOAL>(latticeClosure s).Finite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DistribLattice α<VAR>DistribLattice β<VAR>s : Set α<VAR>t : Set β<GOAL>latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
<VAR>α : Type u<VAR>self : SemilatticeSup α<VAR>a b c : α<GOAL>a ≤ c → b ≤ c → a ⊔ b ≤ c
<VAR>α : Type u<VAR>self : SemilatticeSup α<VAR>a b : α<GOAL>a ≤ a ⊔ b
<VAR>α : Type u<VAR>self : SemilatticeSup α<VAR>a b : α<GOAL>b ≤ a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ≤ a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>b ≤ a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<VAR>h : c ≤ a<GOAL>c ≤ a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<VAR>h : c ≤ b<GOAL>c ≤ a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<VAR>h : c < a<GOAL>c < a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<VAR>h : c < b<GOAL>c < a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ≤ c → b ≤ c → a ⊔ b ≤ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ⊔ b = a ↔ b ≤ a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ⊔ b = b ↔ a ≤ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a = a ⊔ b ↔ b ≤ a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>b = a ⊔ b ↔ a ≤ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a < a ⊔ b ↔ ¬b ≤ a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>b < a ⊔ b ↔ ¬a ≤ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<VAR>h : a ≠ b<GOAL>a < a ⊔ b ∨ b < a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ≤ b ↔ ∃ c, b = a ⊔ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a ⊔ c ≤ b ⊔ d
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<VAR>h₁ : a ≤ b<VAR>c : α<GOAL>c ⊔ a ≤ c ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<VAR>h₁ : a ≤ b<VAR>c : α<GOAL>a ⊔ c ≤ b ⊔ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a : α<GOAL>a ⊔ a = a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ⊔ b = b ⊔ a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ b ⊔ c = c ⊔ b ⊔ a
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ⊔ (a ⊔ b) = a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<GOAL>a ⊔ b ⊔ b = a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ b ⊔ c = a ⊔ c ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c d : α<GOAL>a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<VAR>hb : b ≤ a ⊔ c<VAR>hc : c ≤ a ⊔ b<GOAL>a ⊔ b = a ⊔ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<VAR>ha : a ≤ b ⊔ c<VAR>hb : b ≤ a ⊔ c<GOAL>a ⊔ c = b ⊔ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b c : α<GOAL>a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>a < a ⊔ b ∨ b < a ⊔ b
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>β : Type u_1<VAR>Preorder β<VAR>f g : α → β<VAR>hf : Monotone f<VAR>hg : Antitone g<VAR>h : f ≤ g<VAR>m n : α<GOAL>f m ≤ g n
<VAR>α : Type u_1<VAR>A B : SemilatticeSup α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<VAR>x y : α<GOAL>x ⊔ y = x ⊔ y
<VAR>α : Type u_1<VAR>A B : SemilatticeSup α<VAR>H : ∀ (x y : α), x ≤ y ↔ x ≤ y<GOAL>A = B
<VAR>α : Type u<VAR>SemilatticeSup α<VAR>s s' : α<VAR>P : Prop<VAR>Decidable P<GOAL>(if P then s else s') ≤ s ⊔ s'
<VAR>α : Type u<VAR>self : SemilatticeInf α<VAR>a b c : α<GOAL>a ≤ b → a ≤ c → a ≤ b ⊓ c
<VAR>α : Type u<VAR>self : SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b ≤ a
<VAR>α : Type u<VAR>self : SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b ≤ b
<VAR>α : Type u_1<VAR>H : SemilatticeSup α<GOAL>OrderDual.instSemilatticeSup αᵒᵈ = H
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b ≤ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b ≤ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ≤ b → a ≤ c → a ≤ b ⊓ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<VAR>h : a ≤ c<GOAL>a ⊓ b ≤ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<VAR>h : b ≤ c<GOAL>a ⊓ b ≤ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<VAR>h : a < c<GOAL>a ⊓ b < c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<VAR>h : b < c<GOAL>a ⊓ b < c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b = a ↔ a ≤ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b = b ↔ b ≤ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a = a ⊓ b ↔ a ≤ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>b = a ⊓ b ↔ b ≤ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b < a ↔ ¬a ≤ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b < b ↔ ¬b ≤ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<VAR>h : a ≠ b<GOAL>a ⊓ b < a ∨ a ⊓ b < b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c d : α<VAR>h₁ : a ≤ b<VAR>h₂ : c ≤ d<GOAL>a ⊓ c ≤ b ⊓ d
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a : α<VAR>b c : α<VAR>h : b ≤ c<GOAL>b ⊓ a ≤ c ⊓ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a : α<VAR>b c : α<VAR>h : b ≤ c<GOAL>a ⊓ b ≤ a ⊓ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a : α<GOAL>a ⊓ a = a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b = b ⊓ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ b ⊓ c = c ⊓ b ⊓ a
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ (a ⊓ b) = a ⊓ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ⊓ b ⊓ b = a ⊓ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ b ⊓ c = a ⊓ c ⊓ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c d : α<GOAL>a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c)
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ b ⊓ c = a ⊓ c ⊓ (b ⊓ c)
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<VAR>hb : a ⊓ c ≤ b<VAR>hc : a ⊓ b ≤ c<GOAL>a ⊓ b = a ⊓ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<VAR>h1 : b ⊓ c ≤ a<VAR>h2 : a ⊓ c ≤ b<GOAL>a ⊓ c = b ⊓ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b c : α<GOAL>a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b
<VAR>α : Type u<VAR>SemilatticeInf α<VAR>a b : α<GOAL>a ≠ b → a ⊓ b < a ∨ a ⊓ b < b