ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>k.IsCountablyGenerated<GOAL>Filter.Tendsto f k l ↔ ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>k : Filter α<VAR>l : Filter β<VAR>k.IsCountablyGenerated<GOAL>(∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l) → Filter.Tendsto f k l
<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>l.IsCountablyGenerated<GOAL>(∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Filter.Tendsto x Filter.atTop l → ∀ᶠ (n : ℕ) in Filter.atTop, p (x n)
<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>l.IsCountablyGenerated<GOAL>(∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Filter.Tendsto x Filter.atTop l ∧ ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)
<VAR>ι : Type u_6<VAR>x : ℕ → ι<VAR>p : ι → Prop<VAR>l : Filter ι<VAR>h_tendsto : Filter.Tendsto x Filter.atTop l<VAR>h : ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)<GOAL>∃ ns, Filter.Tendsto (fun n => x (ns n)) Filter.atTop l ∧ ∀ (n : ℕ), p (x (ns n))
<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>l.IsCountablyGenerated<VAR>h : ∃ᶠ (n : ι) in l, p n<GOAL>∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>l.IsCountablyGenerated<GOAL>(∃ᶠ (n : ι) in l, p n) ↔ ∃ ns, Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)
<VAR>α : Type u_3<VAR>ι : Type u_6<VAR>x : ι → α<VAR>f : Filter α<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>hxy : ∀ (ns : ℕ → ι), Filter.Tendsto ns Filter.atTop l → ∃ ms, Filter.Tendsto (fun n => x (ns (ms n))) Filter.atTop f<GOAL>Filter.Tendsto x l f
<VAR>α : Type u_3<VAR>f : Filter α<VAR>f.IsCountablyGenerated<VAR>u : ℕ → α<VAR>hx : (f ⊓ Filter.map u Filter.atTop).NeBot<GOAL>∃ θ, StrictMono θ ∧ Filter.Tendsto (u ∘ θ) Filter.atTop f
<VAR>R : Type u_6<VAR>LinearOrderedSemiring R<VAR>a : R<GOAL>∃ x ≥ 0, a < x * x
<VAR>R : Type u_6<VAR>LinearOrderedSemiring R<VAR>a : R<GOAL>∃ x ≥ 0, a ≤ x * x
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : α → Type u_6<VAR>Preorder ι<VAR>s : ι → Set α<VAR>(i : ι) → DecidablePred fun x => x ∈ s i<VAR>DecidablePred fun x => x ∈ ⋃ i, s i<VAR>hs : Monotone s<VAR>f g : (a : α) → β a<VAR>a : α<GOAL>∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
<VAR>ι : Type u_1<VAR>α : Type u_3<VAR>β : α → Type u_6<VAR>Preorder ι<VAR>s : ι → Set α<VAR>(i : ι) → DecidablePred fun x => x ∈ s i<VAR>DecidablePred fun x => x ∈ ⋂ i, s i<VAR>hs : Antitone s<VAR>f g : (a : α) → β a<VAR>a : α<GOAL>∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>AddCommMonoid α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>f : β → α<VAR>hf : ∀ x ∉ Set.range g, f x = 0<GOAL>Filter.map (fun s => ∑ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun s => ∑ i ∈ s, f i) Filter.atTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>CommMonoid α<VAR>g : γ → β<VAR>hg : Function.Injective g<VAR>f : β → α<VAR>hf : ∀ x ∉ Set.range g, f x = 1<GOAL>Filter.map (fun s => ∏ i ∈ s, f (g i)) Filter.atTop = Filter.map (fun s => ∏ i ∈ s, f i) Filter.atTop
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>ht : t.SupIndep f<VAR>h : s ⊆ t<GOAL>s.SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>f : ι → α<GOAL>∅.SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>i : ι<VAR>f : ι → α<GOAL>{i}.SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.SupIndep f<GOAL>(↑s).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s t : Finset ι<VAR>f : ι → α<VAR>i : ι<VAR>hs : s.SupIndep f<VAR>hts : t ⊆ s<VAR>hi : i ∈ s<VAR>hf : ∀ (i : ι), f i ≠ ⊥<GOAL>f i ≤ t.sup f ↔ i ∈ t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>DecidableEq ι<GOAL>s.SupIndep f ↔ ∀ i ∈ s, Disjoint (f i) ((s.erase i).sup f)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>Lattice α<VAR>OrderBot α<VAR>f : ι → α<VAR>DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → ι<VAR>hs : s.SupIndep (f ∘ g)<GOAL>(Finset.image g s).SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>Lattice α<VAR>OrderBot α<VAR>f : ι → α<VAR>s : Finset ι'<VAR>g : ι' ↪ ι<GOAL>(Finset.map g s).SupIndep f ↔ s.SupIndep (f ∘ ⇑g)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>f : ι → α<VAR>DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>{i, j}.SupIndep f ↔ Disjoint (f i) (f j)
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>f : Bool → α<GOAL>Finset.univ.SupIndep f ↔ Disjoint (f false) (f true)
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>f : Fin 2 → α<GOAL>Finset.univ.SupIndep f ↔ Disjoint (f 0) (f 1)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.SupIndep f<GOAL>s.attach.SupIndep fun a => f ↑a
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Lattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>(s.attach.SupIndep fun a => f ↑a) ↔ s.SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>s.SupIndep f ↔ (↑s).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.SupIndep fun i => (g i).sup f<VAR>hg : ∀ i' ∈ s, (g i').SupIndep f<GOAL>(s.sup g).SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.SupIndep fun i => (g i).sup f<VAR>hg : ∀ i' ∈ s, (g i').SupIndep f<GOAL>(s.biUnion g).SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>DistribLattice α<VAR>OrderBot α<VAR>β : ι → Type u_5<VAR>s : Finset ι<VAR>g : (i : ι) → Finset (β i)<VAR>f : Sigma β → α<VAR>hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩<VAR>hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩<GOAL>(s.sigma g).SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<VAR>hs : s.SupIndep fun i => t.sup fun i' => f (i, i')<VAR>ht : t.SupIndep fun i' => s.sup fun i => f (i, i')<GOAL>(s ×ˢ t).SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>DistribLattice α<VAR>OrderBot α<VAR>s : Finset ι<VAR>t : Finset ι'<VAR>f : ι × ι' → α<GOAL>(s.product t).SupIndep f ↔ (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')
<VAR>α : Type u_1<VAR>CompleteLattice α<GOAL>CompleteLattice.SetIndependent ∅
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>hs : CompleteLattice.SetIndependent s<VAR>t : Set α<VAR>hst : t ⊆ s<GOAL>CompleteLattice.SetIndependent t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>hs : CompleteLattice.SetIndependent s<GOAL>s.PairwiseDisjoint id
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a : α<GOAL>CompleteLattice.SetIndependent {a}
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>a b : α<VAR>hab : a ≠ b<GOAL>CompleteLattice.SetIndependent {a, b} ↔ Disjoint a b
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>s : Set α<VAR>hs : CompleteLattice.SetIndependent s<VAR>x : α<VAR>y : Set α<VAR>hx : x ∈ s<VAR>hy : y ⊆ s<VAR>hxy : x ∉ y<GOAL>Disjoint x (sSup y)
<VAR>α : Type u_5<VAR>CompleteLattice α<VAR>s : Set α<GOAL>CompleteLattice.SetIndependent s ↔ CompleteLattice.Independent Subtype.val
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<GOAL>CompleteLattice.Independent t ↔ ∀ (i : ι), Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<GOAL>CompleteLattice.Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<GOAL>CompleteLattice.Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup {a | ∃ j, j ≠ i ∧ t j = a})
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>t : Empty → α<GOAL>CompleteLattice.Independent t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>t : PEmpty.{u_5} → α<GOAL>CompleteLattice.Independent t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<GOAL>Pairwise (Disjoint on t)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>s t : ι → α<VAR>hs : CompleteLattice.Independent s<VAR>hst : t ≤ s<GOAL>CompleteLattice.Independent t
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>t : ι → α<VAR>f : ι' → ι<VAR>ht : CompleteLattice.Independent t<VAR>hf : Function.Injective f<GOAL>CompleteLattice.Independent (t ∘ f)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>t : ι → α<VAR>f : ι' → ι<VAR>ht : CompleteLattice.Independent (t ∘ f)<VAR>hf : Function.Surjective f<GOAL>CompleteLattice.Independent t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<GOAL>CompleteLattice.SetIndependent (Set.range t)
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<GOAL>(CompleteLattice.Independent fun i => t ↑i) ↔ CompleteLattice.Independent t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<GOAL>Set.InjOn t {i | t i ≠ ⊥}
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<VAR>h_ne_bot : ∀ (i : ι), t i ≠ ⊥<GOAL>Function.Injective t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>t : ι → α<VAR>i j : ι<VAR>hij : i ≠ j<VAR>huniv : ∀ (k : ι), k = i ∨ k = j<GOAL>CompleteLattice.Independent t ↔ Disjoint (t i) (t j)
<VAR>ι : Sort u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>a : ι → α<VAR>ha : CompleteLattice.Independent a<GOAL>CompleteLattice.Independent (⇑f ∘ a)
<VAR>ι : Sort u_5<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CompleteLattice α<VAR>CompleteLattice β<VAR>f : α ≃o β<VAR>a : ι → α<GOAL>CompleteLattice.Independent (⇑f ∘ a) ↔ CompleteLattice.Independent a
<VAR>ι : Type u_5<VAR>α : Type u_6<VAR>CompleteLattice α<VAR>t : ι → α<VAR>ht : CompleteLattice.Independent t<VAR>x : ι<VAR>y : Set ι<VAR>hx : x ∉ y<GOAL>Disjoint (t x) (⨆ i ∈ y, t i)
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>ι : Sort u_5<VAR>a : α<VAR>t : ι → ↑(Set.Iic a)<VAR>ht : CompleteLattice.Independent (Subtype.val ∘ t)<GOAL>CompleteLattice.Independent t
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>s : Finset ι<VAR>f : ι → α<GOAL>CompleteLattice.Independent (f ∘ Subtype.val) ↔ s.SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>f : ι → α<VAR>s : Finset ι<VAR>h : CompleteLattice.Independent f<GOAL>s.SupIndep f
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>CompleteLattice α<VAR>Fintype ι<VAR>f : ι → α<GOAL>CompleteLattice.Independent f ↔ Finset.univ.SupIndep f
<VAR>α : Type u_1<VAR>Order.Frame α<VAR>s : Set α<GOAL>CompleteLattice.SetIndependent s ↔ s.PairwiseDisjoint id
<VAR>α : Type u_1<VAR>ι : Type u_3<VAR>Order.Frame α<VAR>f : ι → α<GOAL>CompleteLattice.Independent f ↔ Pairwise (Disjoint on f)
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddAbove s<VAR>hlim : ¬Order.IsSuccLimit (sSup s)<GOAL>sSup s ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>hne : s.Nonempty<VAR>hbdd : BddBelow s<VAR>hlim : ¬Order.IsPredLimit (sInf s)<GOAL>sInf s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>Nonempty ι<VAR>f : ι → α<VAR>hf : BddAbove (Set.range f)<VAR>hf' : ¬Order.IsSuccLimit (⨆ i, f i)<GOAL>∃ i, f i = ⨆ i, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>Nonempty ι<VAR>f : ι → α<VAR>hf : BddBelow (Set.range f)<VAR>hf' : ¬Order.IsPredLimit (⨅ i, f i)<GOAL>∃ i, f i = ⨅ i, f i
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>x : α<VAR>hs : IsLUB s x<VAR>hne : s.Nonempty<VAR>hx : ¬Order.IsSuccLimit x<GOAL>x ∈ s
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>s : Set α<VAR>x : α<VAR>hs : IsGLB s x<VAR>hne : s.Nonempty<VAR>hx : ¬Order.IsPredLimit x<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>Nonempty ι<VAR>f : ι → α<VAR>x : α<VAR>hf : IsLUB (Set.range f) x<VAR>hx : ¬Order.IsSuccLimit x<GOAL>∃ i, f i = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrder α<VAR>Nonempty ι<VAR>f : ι → α<VAR>x : α<VAR>hf : IsGLB (Set.range f) x<VAR>hx : ¬Order.IsPredLimit x<GOAL>∃ i, f i = x
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>hbdd : BddAbove s<VAR>hlim : ¬Order.IsSuccLimit (sSup s)<GOAL>sSup s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>hf : BddAbove (Set.range f)<VAR>hf' : ¬Order.IsSuccLimit (⨆ i, f i)<GOAL>∃ i, f i = ⨆ i, f i
<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrderBot α<VAR>s : Set α<VAR>x : α<VAR>hs : IsLUB s x<VAR>hx : ¬Order.IsSuccLimit x<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>ConditionallyCompleteLinearOrderBot α<VAR>f : ι → α<VAR>x : α<VAR>hf : IsLUB (Set.range f) x<VAR>hx : ¬Order.IsSuccLimit x<GOAL>∃ i, f i = x
<VAR>α : Type u_2<VAR>CompleteLinearOrder α<VAR>s : Set α<VAR>hlim : ¬Order.IsSuccLimit (sSup s)<GOAL>sSup s ∈ s
<VAR>α : Type u_2<VAR>CompleteLinearOrder α<VAR>s : Set α<VAR>hlim : ¬Order.IsPredLimit (sInf s)<GOAL>sInf s ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CompleteLinearOrder α<VAR>f : ι → α<VAR>hf : ¬Order.IsSuccLimit (⨆ i, f i)<GOAL>∃ i, f i = ⨆ i, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CompleteLinearOrder α<VAR>f : ι → α<VAR>hf : ¬Order.IsPredLimit (⨅ i, f i)<GOAL>∃ i, f i = ⨅ i, f i
<VAR>α : Type u_2<VAR>CompleteLinearOrder α<VAR>s : Set α<VAR>x : α<VAR>hs : IsGLB s x<VAR>hx : ¬Order.IsPredLimit x<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CompleteLinearOrder α<VAR>f : ι → α<VAR>x : α<VAR>hf : IsGLB (Set.range f) x<VAR>hx : ¬Order.IsPredLimit x<GOAL>∃ i, f i = x
<VAR>α : Type u_1<VAR>SemilatticeSup α<VAR>OrderBot α<GOAL>(SemilatSupCat.of α).X = α
<VAR>X : SemilatSupCat<GOAL>↑((CategoryTheory.forget₂ SemilatSupCat PartOrd).obj X) = X.X
<VAR>α : Type u_1<VAR>SemilatticeInf α<VAR>OrderTop α<GOAL>(SemilatInfCat.of α).X = α
<VAR>X : SemilatInfCat<GOAL>↑((CategoryTheory.forget₂ SemilatInfCat PartOrd).obj X) = X.X
<VAR>α β : SemilatSupCat<VAR>e : α.X ≃o β.X<VAR>a : β.X<GOAL>(SemilatSupCat.Iso.mk e).inv.toSupHom a = e.symm a
<VAR>α β : SemilatSupCat<VAR>e : α.X ≃o β.X<VAR>a : α.X<GOAL>(SemilatSupCat.Iso.mk e).hom.toSupHom a = e a
<VAR>X : SemilatSupCat<GOAL>SemilatSupCat.dual.obj X = SemilatInfCat.of X.Xᵒᵈ
<VAR>X Y : SemilatSupCat<VAR>a : SupBotHom X.X Y.X<GOAL>SemilatSupCat.dual.map a = SupBotHom.dual a
<VAR>α β : SemilatInfCat<VAR>e : α.X ≃o β.X<VAR>a : α.X<GOAL>(SemilatInfCat.Iso.mk e).hom.toInfHom a = e a
<VAR>α β : SemilatInfCat<VAR>e : α.X ≃o β.X<VAR>a : β.X<GOAL>(SemilatInfCat.Iso.mk e).inv.toInfHom a = e.symm a
<VAR>X Y : SemilatInfCat<VAR>a : InfTopHom X.X Y.X<GOAL>SemilatInfCat.dual.map a = InfTopHom.dual a
<VAR>X : SemilatInfCat<GOAL>SemilatInfCat.dual.obj X = SemilatSupCat.of X.Xᵒᵈ
<GOAL>SemilatSupCatEquivSemilatInfCat.inverse = SemilatInfCat.dual
<GOAL>SemilatSupCatEquivSemilatInfCat.functor = SemilatSupCat.dual
<GOAL>SemilatSupCat.dual ⋙ CategoryTheory.forget₂ SemilatInfCat PartOrd = CategoryTheory.forget₂ SemilatSupCat PartOrd ⋙ PartOrd.dual
<GOAL>SemilatInfCat.dual ⋙ CategoryTheory.forget₂ SemilatSupCat PartOrd = CategoryTheory.forget₂ SemilatInfCat PartOrd ⋙ PartOrd.dual
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderTop α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c<GOAL>IsCoatomic α
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>OrderBot α<VAR>h : ∀ (c : Set α), IsChain (fun x x_1 => x ≤ x_1) c → c.Nonempty → ⊥ ∉ c → ∃ x, x ≠ ⊥ ∧ x ∈ lowerBounds c<GOAL>IsAtomic α
<VAR>α : Type u<VAR>LE α<VAR>a b : α<GOAL>{ down := a } ≤ { down := b } ↔ a ≤ b
<VAR>α : Type u<VAR>LE α<VAR>a b : ULift.{u_1, u} α<GOAL>a.down ≤ b.down ↔ a ≤ b
<VAR>α : Type u<VAR>LT α<VAR>a b : α<GOAL>{ down := a } < { down := b } ↔ a < b
<VAR>α : Type u<VAR>LT α<VAR>a b : ULift.{u_1, u} α<GOAL>a.down < b.down ↔ a < b
<VAR>α : Type u<VAR>Ord α<VAR>a b : α<GOAL>compare { down := a } { down := b } = compare a b
<VAR>α : Type u<VAR>Ord α<VAR>a b : ULift.{u_1, u} α<GOAL>compare a.down b.down = compare a b
<VAR>α : Type u<VAR>Sup α<VAR>a b : α<GOAL>{ down := a ⊔ b } = { down := a } ⊔ { down := b }
<VAR>α : Type u<VAR>Sup α<VAR>a b : ULift.{u_1, u} α<GOAL>(a ⊔ b).down = a.down ⊔ b.down
<VAR>α : Type u<VAR>Inf α<VAR>a b : α<GOAL>{ down := a ⊓ b } = { down := a } ⊓ { down := b }
<VAR>α : Type u<VAR>Inf α<VAR>a b : ULift.{u_1, u} α<GOAL>(a ⊓ b).down = a.down ⊓ b.down
<VAR>α : Type u<VAR>SDiff α<VAR>a b : α<GOAL>{ down := a \ b } = { down := a } \ { down := b }
<VAR>α : Type u<VAR>SDiff α<VAR>a b : ULift.{u_1, u} α<GOAL>(a \ b).down = a.down \ b.down
<VAR>α : Type u<VAR>HasCompl α<VAR>a : α<GOAL>{ down := aᶜ } = { down := a }ᶜ
<VAR>α : Type u<VAR>HasCompl α<VAR>a : ULift.{u_1, u} α<GOAL>aᶜ.down = a.downᶜ
<VAR>α : Type u_1<VAR>self : Filter α<VAR>x y : Set α<GOAL>x ∈ self.sets → x ⊆ y → y ∈ self.sets
<VAR>α : Type u_1<VAR>self : Filter α<VAR>x y : Set α<GOAL>x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets
<VAR>α : Type u_1<VAR>self : Filter α<GOAL>Set.univ ∈ self.sets
<VAR>α : Type u<VAR>s : Set α<VAR>t : Set (Set α)<VAR>h₁ : Set.univ ∈ t<VAR>h₂ : ∀ {x y : Set α}, x ∈ t → x ⊆ y → y ∈ t<VAR>h₃ : ∀ {x y : Set α}, x ∈ t → y ∈ t → x ∩ y ∈ t<GOAL>s ∈ { sets := t, univ_sets := h₁, sets_of_superset := h₂, inter_sets := h₃ } ↔ s ∈ t
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∈ f.sets ↔ s ∈ f
<VAR>α : Type u<VAR>f g : Filter α<GOAL>f.sets = g.sets → f = g
<VAR>α : Type u<VAR>f g : Filter α<GOAL>f = g ↔ f.sets = g.sets
<VAR>α : Type u<VAR>f g : Filter α<VAR>h : ∀ (s : Set α), s ∈ f ↔ s ∈ g<GOAL>f = g
<VAR>α : Type u<VAR>f g : Filter α<GOAL>f = g ↔ ∀ (s : Set α), s ∈ f ↔ s ∈ g
<VAR>α : Type u<VAR>f g : Filter α<VAR>h : ∀ (s : Set α), sᶜ ∈ f ↔ sᶜ ∈ g<GOAL>f = g
<VAR>α : Type u<VAR>f : Filter α<GOAL>Set.univ ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>x y : Set α<VAR>hx : x ∈ f<VAR>hxy : x ⊆ y<GOAL>y ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<VAR>hs : s ∈ f<VAR>ht : t ∈ f<GOAL>s ∩ t ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<GOAL>s ∩ t ∈ f ↔ s ∈ f ∧ t ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<VAR>hs : s ∈ f<VAR>ht : tᶜ ∈ f<GOAL>s \ t ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<VAR>h : ∀ (a : α), a ∈ s<GOAL>s ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<VAR>hs : s ∈ f<VAR>h : {x | x ∈ s → x ∈ t} ∈ f<GOAL>t ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<VAR>h : {x | x ∈ s ↔ x ∈ t} ∈ f<GOAL>s ∈ f ↔ t ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>S : Set (Set α)<VAR>hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f<GOAL>f.copy S hmem = f
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<VAR>S : Set (Set α)<VAR>hmem : ∀ (s : Set α), s ∈ S ↔ s ∈ f<GOAL>s ∈ f.copy S hmem ↔ s ∈ S
<VAR>α : Type u<VAR>f : Filter α<VAR>β : Type v<VAR>s : β → Set α<VAR>is : Set β<VAR>hf : is.Finite<GOAL>⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>β : Type v<VAR>s : β → Set α<VAR>is : Finset β<GOAL>⋂ i ∈ is, s i ∈ f ↔ ∀ i ∈ is, s i ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set (Set α)<VAR>hfin : s.Finite<GOAL>⋂₀ s ∈ f ↔ ∀ U ∈ s, U ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>β : Sort v<VAR>s : β → Set α<VAR>Finite β<GOAL>⋂ i, s i ∈ f ↔ ∀ (i : β), s i ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<GOAL>(∃ t ∈ f, t ⊆ s) ↔ s ∈ f
<VAR>α : Type u<VAR>f : Filter α<GOAL>Monotone fun s => s ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>P Q : Set α → Prop<VAR>hP : Antitone P<VAR>hQ : Antitone Q<GOAL>((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u
<VAR>α : Type u<VAR>f : Filter α<VAR>β : Type u_1<VAR>p : Set α → β → Prop<GOAL>(∀ a ∈ f, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ f, p a b
<VAR>α : Type u<VAR>s t : Set α<GOAL>s ∈ 𝓟 t ↔ t ⊆ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∈ 𝓟 s
<VAR>α : Type u<VAR>s : Set α<VAR>f : Filter (Filter α)<GOAL>s ∈ f.join ↔ {t | s ∈ t} ∈ f
<VAR>α : Type u<VAR>f g : Filter α<GOAL>f ≤ g ↔ ∀ x ∈ g, x ∈ f
<VAR>α : Type u<VAR>f g : Filter α<GOAL>¬f ≤ g ↔ ∃ s ∈ g, s ∉ f
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>U : Set α<VAR>h : U ∈ s<GOAL>U ∈ Filter.generate s
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>f : Filter α<GOAL>f ≤ Filter.generate s ↔ s ⊆ f.sets
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>U : Set α<GOAL>U ∈ Filter.generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
<VAR>α : Type u<VAR>s : Set α<GOAL>Filter.generate {s} = 𝓟 s
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : (Filter.generate s).sets = s<GOAL>Filter.mkOfClosure s hs = Filter.generate s
<VAR>α : Type u<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, s = t₁ ∩ t₂
<VAR>α : Type u<VAR>f g : Filter α<VAR>s : Set α<VAR>h : s ∈ f<GOAL>s ∈ f ⊓ g
<VAR>α : Type u<VAR>f g : Filter α<VAR>s : Set α<VAR>h : s ∈ g<GOAL>s ∈ f ⊓ g
<VAR>α : Type u<VAR>f g : Filter α<VAR>s t : Set α<VAR>hs : s ∈ f<VAR>ht : t ∈ g<GOAL>s ∩ t ∈ f ⊓ g
<VAR>α : Type u<VAR>f g : Filter α<VAR>s t u : Set α<VAR>hs : s ∈ f<VAR>ht : t ∈ g<VAR>h : s ∩ t ⊆ u<GOAL>u ∈ f ⊓ g
<VAR>α : Type u<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f ⊓ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ∩ t₂ ⊆ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∈ ⊤ ↔ ∀ (x : α), x ∈ s
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∈ ⊤ ↔ s = Set.univ
<VAR>α : Type u<VAR>f : Filter α<VAR>self : f.NeBot<GOAL>f ≠ ⊥
<VAR>α : Type u<VAR>f : Filter α<GOAL>f.NeBot ↔ f ≠ ⊥
<VAR>α : Type u<VAR>f : Filter α<VAR>hf : f.NeBot<GOAL>f ≠ ⊥
<VAR>α : Type u<VAR>f : Filter α<GOAL>¬f.NeBot ↔ f = ⊥
<VAR>α : Type u<VAR>f g : Filter α<VAR>hf : f.NeBot<VAR>hg : f ≤ g<GOAL>g.NeBot
<VAR>α : Type u<VAR>f g : Filter α<GOAL>(f ⊔ g).NeBot ↔ f.NeBot ∨ g.NeBot
<VAR>α : Type u<VAR>f : Filter α<GOAL>¬Disjoint f f ↔ f.NeBot
<VAR>α : Type u<GOAL>⊥.sets = Set.univ
<VAR>α : Type u<VAR>f : Filter α<GOAL>f = ⊥ ∨ f.NeBot
<VAR>α : Type u<VAR>f g : Filter α<GOAL>(f ⊔ g).sets = f.sets ∩ g.sets
<VAR>α : Type u<VAR>s : Set (Filter α)<GOAL>(sSup s).sets = ⋂ f ∈ s, f.sets
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<GOAL>(iSup f).sets = ⋂ i, (f i).sets
<VAR>α : Type u<GOAL>Filter.generate ∅ = ⊤
<VAR>α : Type u<GOAL>Filter.generate Set.univ = ⊥
<VAR>α : Type u<VAR>s t : Set (Set α)<GOAL>Filter.generate (s ∪ t) = Filter.generate s ⊓ Filter.generate t
<VAR>α : Type u<VAR>ι : Sort x<VAR>s : ι → Set (Set α)<GOAL>Filter.generate (⋃ i, s i) = ⨅ i, Filter.generate (s i)
<VAR>α : Type u<VAR>s : Set α<GOAL>s ∈ ⊥
<VAR>α : Type u<VAR>f g : Filter α<VAR>s : Set α<GOAL>s ∈ f ⊔ g ↔ s ∈ f ∧ s ∈ g
<VAR>α : Type u<VAR>f g : Filter α<VAR>s t : Set α<VAR>hs : s ∈ f<VAR>ht : t ∈ g<GOAL>s ∪ t ∈ f ⊔ g
<VAR>α : Type u<VAR>x : Set α<VAR>s : Set (Filter α)<GOAL>x ∈ sSup s ↔ ∀ f ∈ s, x ∈ f
<VAR>α : Type u<VAR>ι : Sort x<VAR>x : Set α<VAR>f : ι → Filter α<GOAL>x ∈ iSup f ↔ ∀ (i : ι), x ∈ f i
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<GOAL>(⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot
<VAR>α : Type u<VAR>ι : Sort x<VAR>s : ι → Filter α<GOAL>iInf s = Filter.generate (⋃ i, (s i).sets)
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>i : ι<VAR>s : Set α<VAR>hs : s ∈ f i<GOAL>s ∈ ⨅ i, f i
<VAR>α : Type u<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<VAR>I : Set ι<VAR>I_fin : I.Finite<VAR>V : ↑I → Set α<VAR>hV : ∀ (i : ↑I), V i ∈ s ↑i<VAR>hU : ⋂ i, V i ⊆ U<GOAL>U ∈ ⨅ i, s i
<VAR>α : Type u<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<GOAL>U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ s ↑i) ∧ U = ⋂ i, V i
<VAR>α : Type u<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<GOAL>U ∈ ⨅ i, s i ↔ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ι), V i ∈ s i) ∧ (∀ i ∉ I, V i = Set.univ) ∧ U = ⋂ i ∈ I, V i ∧ U = ⋂ i, V i
<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>f : ι → Filter α<VAR>s : Set α<VAR>hs : s ∈ ⨅ i, f i<GOAL>∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
<VAR>ι : Type u_2<VAR>Finite ι<VAR>α : Type u_3<VAR>f : ι → Filter α<VAR>s : Set α<GOAL>s ∈ ⨅ i, f i ↔ ∃ t, (∀ (i : ι), t i ∈ f i) ∧ s = ⋂ i, t i
<VAR>α : Type u<VAR>s : Set α<VAR>f : Filter α<GOAL>f ≤ 𝓟 s ↔ s ∈ f
<VAR>α : Type u<VAR>s : Set α<GOAL>Set.Iic (𝓟 s) = {l | s ∈ l}