ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>s.carrier = ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>IsLowerSet ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>↑{ carrier := s, lower' := hs } = s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>hs : IsLowerSet s<VAR>a : α<GOAL>a ∈ { carrier := s, lower' := hs } ↔ a ∈ s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>↑s ⊆ ↑t ↔ t ≤ s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>↑s ⊂ ↑t ↔ t < s
<VAR>α : Type u_1<VAR>LE α<GOAL>↑⊤ = ∅
<VAR>α : Type u_1<VAR>LE α<GOAL>↑⊥ = Set.univ
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>↑s = Set.univ ↔ s = ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>↑s = ∅ ↔ s = ⊤
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>(↑s).Nonempty ↔ s ≠ ⊤
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>↑(s ⊔ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>↑(s ⊓ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (UpperSet α)<GOAL>↑(sSup S) = ⋂ s ∈ S, ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (UpperSet α)<GOAL>↑(sInf S) = ⋃ s ∈ S, ↑s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → UpperSet α<GOAL>↑(⨆ i, f i) = ⋂ i, ↑(f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → UpperSet α<GOAL>↑(⨅ i, f i) = ⋃ i, ↑(f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>↑(⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>a ∉ ⊤
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>a ∈ ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<VAR>a : α<GOAL>a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<VAR>a : α<GOAL>a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (UpperSet α)<VAR>a : α<GOAL>a ∈ sSup S ↔ ∀ s ∈ S, a ∈ s
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (UpperSet α)<VAR>a : α<GOAL>a ∈ sInf S ↔ ∃ s ∈ S, a ∈ s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>a ∈ ⨆ i, f i ↔ ∀ (i : ι), a ∈ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>a ∈ ⨅ i, f i ↔ ∃ i, a ∈ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>Codisjoint ↑s ↑t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>↑s ⊆ ↑t ↔ s ≤ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>↑s ⊂ ↑t ↔ s < t
<VAR>α : Type u_1<VAR>LE α<GOAL>↑⊤ = Set.univ
<VAR>α : Type u_1<VAR>LE α<GOAL>↑⊥ = ∅
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>↑s = Set.univ ↔ s = ⊤
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>↑s = ∅ ↔ s = ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>(↑s).Nonempty ↔ s ≠ ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>↑(s ⊔ t) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>↑(s ⊓ t) = ↑s ∩ ↑t
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (LowerSet α)<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (LowerSet α)<GOAL>↑(sInf S) = ⋂ s ∈ S, ↑s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → LowerSet α<GOAL>↑(⨆ i, f i) = ⋃ i, ↑(f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → LowerSet α<GOAL>↑(⨅ i, f i) = ⋂ i, ↑(f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>↑(⨆ i, ⨆ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>↑(⨅ i, ⨅ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>a ∈ ⊤
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>a ∉ ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<VAR>a : α<GOAL>a ∈ s ⊔ t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<VAR>a : α<GOAL>a ∈ s ⊓ t ↔ a ∈ s ∧ a ∈ t
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (LowerSet α)<VAR>a : α<GOAL>a ∈ sSup S ↔ ∃ s ∈ S, a ∈ s
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (LowerSet α)<VAR>a : α<GOAL>a ∈ sInf S ↔ ∀ s ∈ S, a ∈ s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>a ∈ ⨆ i, f i ↔ ∃ i, a ∈ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>a : α<VAR>f : ι → LowerSet α<GOAL>a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>a ∈ ⨆ i, ⨆ j, f i j ↔ ∃ i j, a ∈ f i j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>a ∈ ⨅ i, ⨅ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>Disjoint ↑s ↑t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>↑s.compl = (↑s)ᶜ
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<VAR>a : α<GOAL>a ∈ s.compl ↔ a ∉ s
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>s.compl.compl = s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>s.compl ≤ t.compl ↔ s ≤ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>(s ⊔ t).compl = s.compl ⊔ t.compl
<VAR>α : Type u_1<VAR>LE α<VAR>s t : UpperSet α<GOAL>(s ⊓ t).compl = s.compl ⊓ t.compl
<VAR>α : Type u_1<VAR>LE α<GOAL>⊤.compl = ⊤
<VAR>α : Type u_1<VAR>LE α<GOAL>⊥.compl = ⊥
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (UpperSet α)<GOAL>(sSup S).compl = ⨆ s ∈ S, s.compl
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (UpperSet α)<GOAL>(sInf S).compl = ⨅ s ∈ S, s.compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → UpperSet α<GOAL>(⨆ i, f i).compl = ⨆ i, (f i).compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → UpperSet α<GOAL>(⨅ i, f i).compl = ⨅ i, (f i).compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>(⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>(⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>↑s.compl = (↑s)ᶜ
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<VAR>a : α<GOAL>a ∈ s.compl ↔ a ∉ s
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>s.compl.compl = s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>s.compl ≤ t.compl ↔ s ≤ t
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>(s ⊔ t).compl = s.compl ⊔ t.compl
<VAR>α : Type u_1<VAR>LE α<VAR>s t : LowerSet α<GOAL>(s ⊓ t).compl = s.compl ⊓ t.compl
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (LowerSet α)<GOAL>(sSup S).compl = ⨆ s ∈ S, s.compl
<VAR>α : Type u_1<VAR>LE α<VAR>S : Set (LowerSet α)<GOAL>(sInf S).compl = ⨅ s ∈ S, s.compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → LowerSet α<GOAL>(⨆ i, f i).compl = ⨆ i, (f i).compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>LE α<VAR>f : ι → LowerSet α<GOAL>(⨅ i, f i).compl = ⨅ i, (f i).compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>(⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>LE α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>(⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl
<VAR>α : Type u_1<VAR>LE α<VAR>s : LowerSet α<GOAL>(RelIso.symm upperSetIsoLowerSet) s = s.compl
<VAR>α : Type u_1<VAR>LE α<VAR>s : UpperSet α<GOAL>upperSetIsoLowerSet s = s.compl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<GOAL>(UpperSet.map f).symm = UpperSet.map f.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : UpperSet α<VAR>b : β<GOAL>b ∈ (UpperSet.map f) s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>Preorder α<GOAL>UpperSet.map (OrderIso.refl α) = OrderIso.refl (UpperSet α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>s : UpperSet α<VAR>g : β ≃o γ<VAR>f : α ≃o β<GOAL>(UpperSet.map g) ((UpperSet.map f) s) = (UpperSet.map (f.trans g)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : UpperSet α<GOAL>↑((UpperSet.map f) s) = ⇑f '' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<GOAL>(LowerSet.map f).symm = LowerSet.map f.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<VAR>f : α ≃o β<VAR>b : β<GOAL>b ∈ (LowerSet.map f) s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>Preorder α<GOAL>LowerSet.map (OrderIso.refl α) = OrderIso.refl (LowerSet α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Preorder α<VAR>Preorder β<VAR>Preorder γ<VAR>s : LowerSet α<VAR>g : β ≃o γ<VAR>f : α ≃o β<GOAL>(LowerSet.map g) ((LowerSet.map f) s) = (LowerSet.map (f.trans g)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : LowerSet α<GOAL>↑((LowerSet.map f) s) = ⇑f '' ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : UpperSet α<GOAL>((UpperSet.map f) s).compl = (LowerSet.map f) s.compl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>s : LowerSet α<GOAL>((LowerSet.map f) s).compl = (UpperSet.map f) s.compl
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>↑(UpperSet.Ici a) = Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>↑(UpperSet.Ioi a) = Set.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ UpperSet.Ici a ↔ a ≤ b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ UpperSet.Ioi a ↔ a < b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>a : α<GOAL>(UpperSet.map f) (UpperSet.Ici a) = UpperSet.Ici (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>a : α<GOAL>(UpperSet.map f) (UpperSet.Ioi a) = UpperSet.Ioi (f a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>UpperSet.Ici a ≤ UpperSet.Ioi a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<GOAL>UpperSet.Ici ⊥ = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<GOAL>UpperSet.Ioi ⊤ = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>UpperSet.Ici a ≠ ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>UpperSet.Ici a < ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>s ≤ UpperSet.Ici a ↔ a ∈ s
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>Function.Injective UpperSet.Ici
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>UpperSet.Ici a = UpperSet.Ici b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>UpperSet.Ici a ≠ UpperSet.Ici b ↔ a ≠ b
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a b : α<GOAL>UpperSet.Ici (a ⊔ b) = UpperSet.Ici a ⊔ UpperSet.Ici b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>S : Set α<GOAL>UpperSet.Ici (sSup S) = ⨆ a ∈ S, UpperSet.Ici a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>UpperSet.Ici (⨆ i, f i) = ⨆ i, UpperSet.Ici (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>UpperSet.Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, UpperSet.Ici (f i j)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>↑(LowerSet.Iic a) = Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>↑(LowerSet.Iio a) = Set.Iio a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ LowerSet.Iic a ↔ b ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>b ∈ LowerSet.Iio a ↔ b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>a : α<GOAL>(LowerSet.map f) (LowerSet.Iic a) = LowerSet.Iic (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>f : α ≃o β<VAR>a : α<GOAL>(LowerSet.map f) (LowerSet.Iio a) = LowerSet.Iio (f a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Ioi a ≤ Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderTop α<GOAL>LowerSet.Iic ⊤ = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>OrderBot α<GOAL>LowerSet.Iio ⊥ = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>LowerSet.Iic a ≠ ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>⊥ < LowerSet.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>LowerSet.Iic a ≤ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>Function.Injective LowerSet.Iic
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>LowerSet.Iic a = LowerSet.Iic b ↔ a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<GOAL>LowerSet.Iic a ≠ LowerSet.Iic b ↔ a ≠ b
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>a b : α<GOAL>LowerSet.Iic (a ⊓ b) = LowerSet.Iic a ⊓ LowerSet.Iic b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>S : Set α<GOAL>LowerSet.Iic (sInf S) = ⨅ a ∈ S, LowerSet.Iic a
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>CompleteLattice α<VAR>f : ι → α<GOAL>LowerSet.Iic (⨅ i, f i) = ⨅ i, LowerSet.Iic (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>LowerSet.Iic (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, LowerSet.Iic (f i j)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ upperClosure s ↔ ∃ a ∈ s, a ≤ x
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ lowerClosure s ↔ ∃ a ∈ s, x ≤ a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>↑(upperClosure s) = ⋃ a ∈ s, Set.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>↑(lowerClosure s) = ⋃ a ∈ s, Set.Iic a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>s ⊆ ↑(upperClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>s ⊆ ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : IsUpperSet t<GOAL>↑(upperClosure s) ⊆ t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : IsLowerSet t<GOAL>↑(lowerClosure s) ⊆ t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : IsUpperSet s<GOAL>↑(upperClosure s) = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>hs : IsLowerSet s<GOAL>↑(lowerClosure s) = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<GOAL>upperClosure ↑s = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<GOAL>lowerClosure ↑s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>f : α ≃o β<GOAL>upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>f : α ≃o β<GOAL>lowerClosure (⇑f '' s) = (LowerSet.map f) (lowerClosure s)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>⨅ a ∈ s, UpperSet.Ici a = upperClosure s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>⨆ a ∈ s, LowerSet.Iic a = lowerClosure s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>t : LowerSet α<GOAL>lowerClosure s ≤ t ↔ s ⊆ ↑t
<VAR>α : Type u_1<VAR>Preorder α<VAR>t : Set α<VAR>s : UpperSet α<GOAL>s ≤ upperClosure t ↔ t ⊆ ↑s
<VAR>α : Type u_1<VAR>Preorder α<GOAL>GaloisConnection (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)
<VAR>α : Type u_1<VAR>Preorder α<GOAL>GaloisConnection lowerClosure SetLike.coe
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Antitone upperClosure
<VAR>α : Type u_1<VAR>Preorder α<GOAL>Monotone lowerClosure
<VAR>α : Type u_1<VAR>Preorder α<GOAL>upperClosure ∅ = ⊤
<VAR>α : Type u_1<VAR>Preorder α<GOAL>lowerClosure ∅ = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>upperClosure {a} = UpperSet.Ici a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>lowerClosure {a} = LowerSet.Iic a
<VAR>α : Type u_1<VAR>Preorder α<GOAL>upperClosure Set.univ = ⊥
<VAR>α : Type u_1<VAR>Preorder α<GOAL>lowerClosure Set.univ = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>upperClosure s = ⊤ ↔ s = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>lowerClosure s = ⊥ ↔ s = ∅
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<GOAL>upperClosure (s ∪ t) = upperClosure s ⊓ upperClosure t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<GOAL>lowerClosure (s ∪ t) = lowerClosure s ⊔ lowerClosure t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>f : ι → Set α<GOAL>upperClosure (⋃ i, f i) = ⨅ i, upperClosure (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>Preorder α<VAR>f : ι → Set α<GOAL>lowerClosure (⋃ i, f i) = ⨆ i, lowerClosure (f i)
<VAR>α : Type u_1<VAR>Preorder α<VAR>S : Set (Set α)<GOAL>upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s
<VAR>α : Type u_1<VAR>Preorder α<VAR>S : Set (Set α)<GOAL>lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>↑(upperClosure s) ∩ ↑(lowerClosure s) = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>upperBounds ↑(lowerClosure s) = upperBounds s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>lowerBounds ↑(upperClosure s) = lowerBounds s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>BddAbove ↑(lowerClosure s) ↔ BddAbove s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>BddBelow ↑(upperClosure s) ↔ BddBelow s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>ht : IsLowerSet t<GOAL>Disjoint (↑(upperClosure s)) t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>hs : IsLowerSet s<GOAL>Disjoint s ↑(upperClosure t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>ht : IsUpperSet t<GOAL>Disjoint (↑(lowerClosure s)) t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s t : Set α<VAR>hs : IsUpperSet s<GOAL>Disjoint s ↑(lowerClosure t) ↔ Disjoint s t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>↑(upperClosure s) = s ↔ IsUpperSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : Set α<GOAL>↑(lowerClosure s) = s ↔ IsLowerSet s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<GOAL>↑(s.sdiff t) = ↑s \ ↑(upperClosure t)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>↑(s.erase a) = ↑s \ ↑(UpperSet.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>s.sdiff {a} = s.erase a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<GOAL>s.sdiff t ≤ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>s.erase a ≤ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<GOAL>s.sdiff t = s ↔ Disjoint (↑s) t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>s.erase a = s ↔ a ∉ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<GOAL>s.sdiff t < s ↔ ¬Disjoint (↑s) t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>s.erase a < s ↔ a ∈ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<GOAL>(s.sdiff t).sdiff t = s.sdiff t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<GOAL>(s.erase a).erase a = s.erase a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t<GOAL>s.sdiff t ⊔ lowerClosure t = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t<GOAL>lowerClosure t ⊔ s.sdiff t = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, a ≤ b → b = a<GOAL>s.erase a ⊔ LowerSet.Iic a = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : LowerSet α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, a ≤ b → b = a<GOAL>LowerSet.Iic a ⊔ s.erase a = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<GOAL>↑(s.sdiff t) = ↑s \ ↑(lowerClosure t)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>↑(s.erase a) = ↑s \ ↑(LowerSet.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>s.sdiff {a} = s.erase a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<GOAL>s ≤ s.sdiff t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>s ≤ s.erase a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<GOAL>s.sdiff t = s ↔ Disjoint (↑s) t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>s.erase a = s ↔ a ∉ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<GOAL>s < s.sdiff t ↔ ¬Disjoint (↑s) t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>s < s.erase a ↔ a ∈ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<GOAL>(s.sdiff t).sdiff t = s.sdiff t
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<GOAL>(s.erase a).erase a = s.erase a
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t<GOAL>s.sdiff t ⊓ upperClosure t = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t<GOAL>upperClosure t ⊓ s.sdiff t = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, b ≤ a → b = a<GOAL>s.erase a ⊓ UpperSet.Ici a = s
<VAR>α : Type u_1<VAR>Preorder α<VAR>s : UpperSet α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, b ≤ a → b = a<GOAL>UpperSet.Ici a ⊓ s.erase a = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsUpperSet s<VAR>ht : IsUpperSet t<GOAL>IsUpperSet (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : Set α<VAR>t : Set β<VAR>hs : IsLowerSet s<VAR>ht : IsLowerSet t<GOAL>IsLowerSet (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : UpperSet α<VAR>t : UpperSet β<GOAL>↑(s ×ˢ t) = ↑s ×ˢ ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>s : UpperSet α<VAR>t : UpperSet β<GOAL>x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<GOAL>UpperSet.Ici x = UpperSet.Ici x.1 ×ˢ UpperSet.Ici x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<GOAL>UpperSet.Ici a ×ˢ UpperSet.Ici b = UpperSet.Ici (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : UpperSet α<GOAL>s ×ˢ ⊤ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>t : UpperSet β<GOAL>⊤ ×ˢ t = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<GOAL>⊥ ×ˢ ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t : UpperSet β<GOAL>(s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>s ×ˢ (t₁ ⊔ t₂) = s ×ˢ t₁ ⊔ s ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t : UpperSet β<GOAL>(s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>s₁ ≤ s₂ → t₁ ≤ t₂ → s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t : UpperSet β<GOAL>s₁ ≤ s₂ → s₁ ×ˢ t ≤ s₂ ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>t₁ ≤ t₂ → s ×ˢ t₁ ≤ s ×ˢ t₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>s₁ s₂ : UpperSet α<GOAL>s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂
<VAR>α : Type u_1<VAR>Preorder α<VAR>s₁ s₂ : UpperSet α<GOAL>s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₂ = ⊤ ∨ t₂ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : UpperSet α<VAR>t : UpperSet β<GOAL>s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s₁ s₂ : UpperSet α<VAR>t₁ t₂ : UpperSet β<GOAL>Codisjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Codisjoint s₁ s₂ ∨ Codisjoint t₁ t₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>s : LowerSet α<VAR>t : LowerSet β<GOAL>↑(s ×ˢ t) = ↑s ×ˢ ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>s : LowerSet α<VAR>t : LowerSet β<GOAL>x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t