ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>Function.Injective fun c => c.toProd.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>c.toProd.1 ⊆ d.toProd.1 ↔ c ≤ d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>c.toProd.1 ⊂ d.toProd.1 ↔ c < d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>c.toProd.2 ⊆ d.toProd.2 ↔ d ≤ c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>c.toProd.2 ⊂ d.toProd.2 ↔ d < c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>StrictMono (Prod.fst ∘ Concept.toProd)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>StrictAnti (Prod.snd ∘ Concept.toProd)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>⊤.toProd.1 = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>⊤.toProd.2 = intentClosure r Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>⊥.toProd.1 = extentClosure r Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>⊥.toProd.2 = Set.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>(c ⊔ d).toProd.1 = extentClosure r (c.toProd.2 ∩ d.toProd.2)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>(c ⊔ d).toProd.2 = c.toProd.2 ∩ d.toProd.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>(c ⊓ d).toProd.1 = c.toProd.1 ∩ d.toProd.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>(c ⊓ d).toProd.2 = intentClosure r (c.toProd.1 ∩ d.toProd.1)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>S : Set (Concept α β r)<GOAL>(sSup S).toProd.1 = extentClosure r (⋂ c ∈ S, c.toProd.2)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>S : Set (Concept α β r)<GOAL>(sSup S).toProd.2 = ⋂ c ∈ S, c.toProd.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>S : Set (Concept α β r)<GOAL>(sInf S).toProd.1 = ⋂ c ∈ S, c.toProd.1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>S : Set (Concept α β r)<GOAL>(sInf S).toProd.2 = intentClosure r (⋂ c ∈ S, c.toProd.1)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c : Concept α β r<GOAL>c.swap.toProd = c.swap
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c : Concept α β r<GOAL>c.swap.swap = c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>c.swap ≤ d.swap ↔ d ≤ c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<VAR>c d : Concept α β r<GOAL>c.swap < d.swap ↔ d < c
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>∀ (a : Concept β α (Function.swap r)), (RelIso.symm Concept.swapEquiv) a = (⇑OrderDual.toDual ∘ Concept.swap) a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>r : α → β → Prop<GOAL>∀ (a : (Concept α β r)ᵒᵈ), Concept.swapEquiv a = (Concept.swap ∘ ⇑OrderDual.ofDual) a
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Set α<GOAL>s ∈ Filter.cocardinal α hreg ↔ #↑sᶜ < c
<VAR>α : Type u<GOAL>Filter.cocardinal α Cardinal.isRegular_aleph0 = Filter.cofinite
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in Filter.cocardinal α hreg, p x) ↔ #↑{x | ¬p x} < c
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<GOAL>(Filter.cocardinal α hreg).HasBasis {s | #↑s < c} compl
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in Filter.cocardinal α hreg, p x) ↔ c ≤ #↑{x | p x}
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Set α<GOAL>(∃ᶠ (x : α) in Filter.cocardinal α hreg, x ∈ s) ↔ c ≤ #↑s
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Set α<GOAL>(Filter.cocardinal α hreg ⊓ 𝓟 s).NeBot ↔ c ≤ #↑s
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Set α<VAR>hs : #↑s < c<GOAL>sᶜ ∈ Filter.cocardinal α hreg
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Set α<VAR>hs : s.Finite<GOAL>sᶜ ∈ Filter.cocardinal α hreg
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Set α<VAR>hs : #↑s < c<GOAL>∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>s : Finset α<GOAL>∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s
<VAR>α : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>x : α<GOAL>∀ᶠ (a : α) in Filter.cocardinal α hreg, a ≠ x
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∈ Filter.cocountable ↔ sᶜ.Countable
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>hs : Set.Bounded r t<GOAL>Set.Bounded r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>hs : Set.Unbounded r s<GOAL>Set.Unbounded r t
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : ∀ (a : α), ∃ b ∈ s, a < b<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) s ↔ ∀ (a : α), ∃ b ∈ s, a < b
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : ∀ (a : α), ∃ b ∈ s, a ≤ b<GOAL>Set.Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) s ↔ ∀ (a : α), ∃ b ∈ s, a ≤ b
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : ∀ (a : α), ∃ b ∈ s, b < a<GOAL>Set.Unbounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<GOAL>Set.Unbounded (fun x x_1 => x ≥ x_1) s ↔ ∀ (a : α), ∃ b ∈ s, b < a
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : ∀ (a : α), ∃ b ∈ s, b ≤ a<GOAL>Set.Unbounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<GOAL>Set.Unbounded (fun x x_1 => x > x_1) s ↔ ∀ (a : α), ∃ b ∈ s, b ≤ a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>r' : α → α → Prop<VAR>h : Set.Bounded r s<VAR>hrr' : r ≤ r'<GOAL>Set.Bounded r' s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : Set.Bounded (fun x x_1 => x < x_1) s<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>r' : α → α → Prop<VAR>hr : r' ≤ r<VAR>h : Set.Unbounded r s<GOAL>Set.Unbounded r' s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : Set.Unbounded (fun x x_1 => x ≤ x_1) s<GOAL>Set.Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>NoMaxOrder α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) s ↔ Set.Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>NoMaxOrder α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) s ↔ Set.Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : Set.Bounded (fun x x_1 => x > x_1) s<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>h : Set.Unbounded (fun x x_1 => x ≥ x_1) s<GOAL>Set.Unbounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>NoMinOrder α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) s ↔ Set.Bounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Preorder α<VAR>NoMinOrder α<GOAL>Set.Unbounded (fun x x_1 => x > x_1) s ↔ Set.Unbounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>LE α<VAR>NoTopOrder α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoTopOrder α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) Set.univ
<VAR>α : Type u_1<VAR>LE α<VAR>NoBotOrder α<GOAL>Set.Unbounded (fun x x_1 => x ≥ x_1) Set.univ
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoBotOrder α<GOAL>Set.Unbounded (fun x x_1 => x > x_1) Set.univ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>Set.Bounded r {b | r b a}
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (Set.Iio a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Iio a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (Set.Iic a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (Set.Ioi a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ioi a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (Set.Ici a)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (Set.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (Set.Ico a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Ico a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (Set.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (Set.Ico a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (Set.Icc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ioo a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ioc a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Ico a b)
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (Set.Icc a b)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) (Set.Ioi a)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) (Set.Ici a)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (Set.Ioi a)
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (Set.Ici a)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m<VAR>a : α<GOAL>Set.Bounded r (s ∩ {b | ¬r b a}) ↔ Set.Bounded r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>H : ∀ (a b : α), ∃ m, ∀ (c : α), r c a ∨ r c b → r c m<VAR>a : α<GOAL>Set.Unbounded r (s ∩ {b | ¬r b a}) ↔ Set.Unbounded r s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeSup α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | ¬b ≤ a}) ↔ Set.Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeSup α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | ¬b ≤ a}) ↔ Set.Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Set.Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Set.Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Set.Bounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a ≤ b}) ↔ Set.Unbounded (fun x x_1 => x ≤ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeSup α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Set.Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeSup α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (s ∩ {b | ¬b < a}) ↔ Set.Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (s ∩ {b | a ≤ b}) ↔ Set.Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (s ∩ {b | a ≤ b}) ↔ Set.Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Set.Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (s ∩ {b | a < b}) ↔ Set.Unbounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeInf α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (s ∩ {b | ¬a ≤ b}) ↔ Set.Bounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeInf α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≥ x_1) (s ∩ {b | ¬a ≤ b}) ↔ Set.Unbounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (s ∩ {b | b < a}) ↔ Set.Bounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≥ x_1) (s ∩ {b | b < a}) ↔ Set.Unbounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x ≥ x_1) (s ∩ {b | b ≤ a}) ↔ Set.Bounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x ≥ x_1) (s ∩ {b | b ≤ a}) ↔ Set.Unbounded (fun x x_1 => x ≥ x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeInf α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (s ∩ {b | ¬a < b}) ↔ Set.Bounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>SemilatticeInf α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x > x_1) (s ∩ {b | ¬a < b}) ↔ Set.Unbounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (s ∩ {b | b ≤ a}) ↔ Set.Bounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x > x_1) (s ∩ {b | b ≤ a}) ↔ Set.Unbounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Set.Bounded (fun x x_1 => x > x_1) (s ∩ {b | b < a}) ↔ Set.Bounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LinearOrder α<VAR>NoMinOrder α<VAR>a : α<GOAL>Set.Unbounded (fun x x_1 => x > x_1) (s ∩ {b | b < a}) ↔ Set.Unbounded (fun x x_1 => x > x_1) s
<VAR>α : Type u_6<VAR>self : FilterBasis α<VAR>x y : Set α<GOAL>x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
<VAR>α : Type u_6<VAR>self : FilterBasis α<GOAL>self.sets.Nonempty
<VAR>α : Type u_1<VAR>s : Set α<VAR>B : FilterBasis α<GOAL>s ∈ B.sets ↔ s ∈ B
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>self : Filter.IsBasis p s<GOAL>∃ i, p i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>self : Filter.IsBasis p s<VAR>i j : ι<GOAL>p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : Filter.IsBasis p s<VAR>U : Set α<GOAL>U ∈ h.filterBasis ↔ ∃ i, p i ∧ s i = U
<VAR>α : Type u_1<VAR>B : FilterBasis α<VAR>U : Set α<GOAL>U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U
<VAR>α : Type u_1<VAR>B : FilterBasis α<VAR>U : Set α<GOAL>U ∈ B → U ∈ B.filter
<VAR>α : Type u_1<VAR>B : FilterBasis α<GOAL>B.filter = ⨅ s, 𝓟 ↑s
<VAR>α : Type u_1<VAR>B : FilterBasis α<GOAL>Filter.generate B.sets = B.filter
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : Filter.IsBasis p s<VAR>U : Set α<GOAL>U ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ U
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : Filter.IsBasis p s<GOAL>h.filter = Filter.generate {U | ∃ i, p i ∧ s i = U}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>self : l.HasBasis p s<VAR>t : Set α<GOAL>t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>(Filter.generate s).HasBasis (fun t => t.Finite ∧ t ⊆ s) fun t => ⋂₀ t
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>(Filter.FilterBasis.ofSets s).sets = Set.sInter '' {t | t.Finite ∧ t ⊆ s}
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>hl : l.HasBasis p s<GOAL>t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p s<GOAL>l = l'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<GOAL>l.HasBasis p s ↔ ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>∃ i, p i
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>Nonempty ι
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : Filter.IsBasis p s<GOAL>h.filter.HasBasis p s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>hl : l.HasBasis p s<VAR>hi : p i<VAR>ht : s i ⊆ t<GOAL>t ∈ l
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>i : ι<VAR>hl : l.HasBasis p s<VAR>hi : p i<GOAL>s i ∈ l
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>h : l.HasBasis p s<VAR>ht : t ∈ l<GOAL>p ↑(h.index t ht)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>h : l.HasBasis p s<VAR>ht : t ∈ l<GOAL>s ↑(h.index t ht) ∈ l
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>h : l.HasBasis p s<VAR>ht : t ∈ l<GOAL>s ↑(h.index t ht) ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>Filter.IsBasis p s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>⋯.filter = l
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l = Filter.generate {U | ∃ i, p i ∧ s i = U}
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>Filter.generate s = Filter.generate (Set.sInter '' {t | t.Finite ∧ t ⊆ s})
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>(Filter.FilterBasis.ofSets s).filter = Filter.generate s
<VAR>α : Type u_1<VAR>B : FilterBasis α<GOAL>B.filter.HasBasis (fun s => s ∈ B) id
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → s' i' ∈ l<GOAL>l.HasBasis p' s'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'<GOAL>l.HasBasis p' s'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>p' : ι → Prop<VAR>s' : ι → Set α<VAR>hp : ∀ (i : ι), p i ↔ p' i<VAR>hs : ∀ (i : ι), p i → s i = s' i<GOAL>l.HasBasis p' s'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>t : ι → Set α<VAR>h : ∀ (i : ι), p i → t i ⊆ s i<VAR>ht : ∀ (i : ι), p i → t i ∈ l<GOAL>l.HasBasis p t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>q : α → Prop<GOAL>(∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x ∈ s i, q x
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>P : Set α → Prop<VAR>mono : ∀ ⦃s t : Set α⦄, s ⊆ t → P t → P s<GOAL>(∃ s ∈ l, P s) ↔ ∃ i, p i ∧ P (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<VAR>P : Set α → Prop<VAR>mono : ∀ ⦃s t : Set α⦄, s ⊆ t → P s → P t<GOAL>(∀ s ∈ l, P s) ↔ ∀ (i : ι), p i → P (s i)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<GOAL>l.NeBot ↔ ∀ {i : ι}, p i → (s i).Nonempty
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<GOAL>l = ⊥ ↔ ∃ i, p i ∧ s i = ∅
<VAR>α : Type u_1<VAR>s : Set (Set α)<GOAL>(Filter.generate s).NeBot ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
<VAR>α : Type u_1<VAR>l : Filter α<GOAL>l.HasBasis (fun s => s ∈ l) id
<VAR>α : Type u_1<VAR>f : Filter α<GOAL>f.asBasis.filter = f
<VAR>α : Type u_1<VAR>l : Filter α<VAR>P : Set α → Prop<GOAL>l.HasBasis (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<VAR>g : ι' → ι<VAR>hg : Function.Surjective g<GOAL>l.HasBasis (p ∘ g) (s ∘ g)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<VAR>e : ι' ≃ ι<GOAL>l.HasBasis (p ∘ ⇑e) (s ∘ ⇑e)
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l.HasBasis (fun t => ∃ i, p i ∧ s i = t) id
<VAR>α : Type u_1<VAR>l : Filter α<VAR>ι : Type u_6<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<GOAL>l.HasBasis (fun x => x ∈ s '' {i | p i}) id
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<VAR>q : ι → Prop<VAR>hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i<GOAL>l.HasBasis (fun i => p i ∧ q i) s
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>h : l.HasBasis p s<VAR>V : Set α<VAR>hV : V ∈ l<GOAL>l.HasBasis (fun i => p i ∧ s i ⊆ V) s
<VAR>α : Type u_1<VAR>l : Filter α<VAR>p : Set α → Prop<VAR>h : l.HasBasis (fun s => s ∈ l ∧ p s) id<VAR>V : Set α<VAR>hV : V ∈ l<GOAL>l.HasBasis (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id
<VAR>α : Type u_1<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl' : l'.HasBasis p' s'<GOAL>l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hl : l.HasBasis p s<GOAL>l ≤ l' ↔ ∀ t ∈ l', ∃ i, p i ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'<GOAL>l = l'
<VAR>α : Type u_1<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>(l ⊓ l').HasBasis (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd
<VAR>α : Type u_1<VAR>l l' : Filter α<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<GOAL>(l ⊓ l').HasBasis (fun i => p i.1 ∧ p' i.2) fun i => s i.1 ∩ s' i.2