ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>f.withTopWithBot.toLatticeHom = f.withBot.withTop
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<GOAL>⇑f.withTopWithBot = Option.map (Option.map ⇑f)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>f : LatticeHom α β<VAR>a : WithTop (WithBot α)<GOAL>f.withTopWithBot a = WithTop.map (Option.map ⇑f) a
<VAR>α : Type u_3<VAR>Lattice α<GOAL>(LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id (WithTop (WithBot α))
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Lattice α<VAR>Lattice β<VAR>Lattice γ<VAR>f : LatticeHom β γ<VAR>g : LatticeHom α β<GOAL>(f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>OrderTop β<VAR>f : LatticeHom α β<GOAL>f.withTop'.toSupHom = f.withTop'
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>OrderBot β<VAR>f : LatticeHom α β<GOAL>f.withBot'.toSupHom = f.withBot'.toSupHom
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Lattice α<VAR>Lattice β<VAR>BoundedOrder β<VAR>f : LatticeHom α β<GOAL>f.withTopWithBot'.toLatticeHom = f.withBot'.withTop'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<GOAL>(∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>p : α × β → Prop<GOAL>(∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<VAR>s : Set (α × β)<GOAL>s ∈ f.curry g ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, (x, y) ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : Filter α<VAR>g : Filter β<GOAL>f.curry g ≤ f.prod g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>la : Filter α<VAR>lb : Filter β<VAR>lc : Filter γ<VAR>h : ∀ᶠ (a : α) in la, Filter.Tendsto (fun b => f a b) lb lc<GOAL>Filter.Tendsto (↿f) (la.curry lb) lc
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>s : Set α<VAR>t : Set β<GOAL>(∃ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ sᶜ ∉ l ∧ tᶜ ∉ m
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s ∈ l<VAR>ht : t ∈ m<GOAL>s ×ˢ t ∈ l.curry m
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>l.NeBot<VAR>m.NeBot<VAR>s : Set α<VAR>t : Set β<GOAL>(∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>self : Finpartition a<GOAL>self.parts.SupIndep id
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>self : Finpartition a<GOAL>self.parts.sup id = a
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>self : Finpartition a<GOAL>⊥ ∉ self.parts
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a : α<VAR>parts : Finset α<VAR>sup_indep : parts.SupIndep id<VAR>sup_parts : parts.sup id = a<GOAL>(Finpartition.ofErase parts sup_indep sup_parts).parts = parts.erase ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a b : α<VAR>P : Finpartition a<VAR>parts : Finset α<VAR>subset : parts ⊆ P.parts<VAR>sup_parts : parts.sup id = b<GOAL>(P.ofSubset subset sup_parts).parts = parts
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a b : α<VAR>P : Finpartition a<VAR>h : a = b<GOAL>(P.copy h).parts = P.parts
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>β : Type u_2<VAR>Lattice β<VAR>OrderBot β<VAR>a : α<VAR>e : α ≃o β<VAR>P : Finpartition a<GOAL>(Finpartition.map e P).parts = Finset.map (↑e).toEmbedding P.parts
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<GOAL>(Finpartition.empty α).parts = ∅
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<GOAL>default = Finpartition.empty α
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>ha : a ≠ ⊥<GOAL>(Finpartition.indiscrete ha).parts = {a}
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>b : α<VAR>hb : b ∈ P.parts<GOAL>b ≤ a
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>b : α<VAR>hb : b ∈ P.parts<GOAL>b ≠ ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>P : Finpartition a<GOAL>(↑P.parts).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>P : Finpartition a<GOAL>P.parts = ∅ ↔ a = ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>P : Finpartition a<GOAL>P.parts.Nonempty ↔ a ≠ ⊥
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>P : Finpartition a<VAR>ha : a ≠ ⊥<GOAL>P.parts.Nonempty
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>Decidable (a = ⊥)<GOAL>⊤.parts ⊆ {a}
<VAR>α : Type u_1<VAR>Lattice α<VAR>OrderBot α<VAR>a : α<VAR>Decidable (a = ⊥)<GOAL>(↑⊤.parts).Subsingleton
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a : α<VAR>P Q : Finpartition a<GOAL>(P ⊓ Q).parts = (Finset.image (fun bc => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase ⊥
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a b : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<VAR>hb : b ∈ Q.parts<GOAL>∃ c ∈ P.parts, c ≤ b
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>a : α<VAR>P Q : Finpartition a<VAR>h : P ≤ Q<GOAL>Q.parts.card ≤ P.parts.card
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a : α<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(P.bind Q).parts = P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a b : α<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a : α<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>hb : b ≠ ⊥<VAR>hab : Disjoint a b<VAR>hc : a ⊔ b = c<GOAL>(P.extend hb hab hc).parts = insert b P.parts
<VAR>α : Type u_1<VAR>DistribLattice α<VAR>OrderBot α<VAR>DecidableEq α<VAR>a : α<VAR>P : Finpartition a<VAR>b c : α<VAR>hb : b ≠ ⊥<VAR>hab : Disjoint a b<VAR>hc : a ⊔ b = c<GOAL>(P.extend hb hab hc).parts.card = P.parts.card + 1
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableEq α<VAR>a : α<VAR>P : Finpartition a<VAR>b : α<GOAL>(P.avoid b).parts.val = (Multiset.map (fun x => x \ b) P.parts.val).dedup.erase ⊥
<VAR>α : Type u_1<VAR>GeneralizedBooleanAlgebra α<VAR>DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<GOAL>c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>a : Finset α<VAR>ha : a ∈ P.parts<GOAL>a.Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ht : t ∈ P.parts<VAR>hu : u ∈ P.parts<VAR>hat : a ∈ t<VAR>hau : a ∈ u<GOAL>t = u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>∃ t ∈ P.parts, a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>P.parts.biUnion id = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>∃! t, t ∈ P.parts ∧ a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>P.part a ∈ P.parts
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>a ∈ P.part a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ht : t ∈ P.parts<VAR>hat : a ∈ t<GOAL>P.part a = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a ∈ P.part b ↔ P.part a = P.part b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>Set.SurjOn P.part ↑s ↑P.parts
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>∃ r ⊆ s, Set.BijOn P.part ↑r ↑P.parts
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>∃ f, ∀ (a b : { x // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>∑ i ∈ P.parts, i.card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>⊥.parts = Finset.map { toFun := singleton, inj' := ⋯ } s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>⊥.parts.card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>t ∈ ⊥.parts ↔ ∃ a ∈ s, {a} = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>P.parts.card ≤ s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>P : Finpartition s<GOAL>s.card % P.parts.card ≤ P.parts.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>Fintype α<VAR>s : Setoid α<VAR>DecidableRel Setoid.r<VAR>b : α<GOAL>b ∈ (Finpartition.ofSetoid s).part a ↔ Setoid.r a b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>Fintype α<VAR>F : Finset (Finset α)<GOAL>t ∈ (Finpartition.atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, Finset.filter (fun i => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>Fintype α<VAR>hs : s.Nonempty<GOAL>(Finpartition.atomise s ∅).parts = {s}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>Fintype α<VAR>F : Finset (Finset α)<GOAL>(Finpartition.atomise s F).parts.card ≤ 2 ^ F.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<VAR>hts : t ⊆ s<GOAL>(Finset.filter (fun u => u ⊆ t ∧ u.Nonempty) (Finpartition.atomise s F).parts).biUnion id = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>Fintype α<VAR>F : Finset (Finset α)<VAR>ht : t ∈ F<GOAL>(Finset.filter (fun u => u ⊆ t ∧ u.Nonempty) (Finpartition.atomise s F).parts).card ≤ 2 ^ (F.card - 1)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>CountableInterFilter f<VAR>u : α → ℝ≥0∞<GOAL>∀ᶠ (y : α) in f, u y ≤ Filter.limsup u f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>CountableInterFilter f<VAR>u : α → ℝ≥0∞<GOAL>Filter.limsup u f = 0 ↔ u =ᶠ[f] 0
<VAR>α : Type u_1<VAR>f : Filter α<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<VAR>ha_top : a ≠ ⊤<GOAL>Filter.limsup (fun x => a * u x) f = a * Filter.limsup u f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>CountableInterFilter f<VAR>u : α → ℝ≥0∞<VAR>a : ℝ≥0∞<GOAL>Filter.limsup (fun x => a * u x) f = a * Filter.limsup u f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>CountableInterFilter f<VAR>u v : α → ℝ≥0∞<GOAL>Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>CountableInterFilter f<VAR>u v : α → ℝ≥0∞<GOAL>Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Countable β<VAR>f : Filter α<VAR>CountableInterFilter f<VAR>g : Filter β<VAR>u : α → β → ℝ≥0∞<GOAL>Filter.limsup (fun a => Filter.liminf (fun b => u a b) g) f ≤ Filter.liminf (fun b => Filter.limsup (fun a => u a b) f) g
<VAR>α : Type u_2<VAR>self : Ultrafilter α<GOAL>(↑self).NeBot
<VAR>α : Type u_2<VAR>self : Ultrafilter α<VAR>g : Filter α<GOAL>g.NeBot → g ≤ ↑self → ↑self ≤ g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>g : Filter α<VAR>h : g ≤ ↑f<VAR>hne : g.NeBot := by infer_instance<GOAL>g = ↑f
<VAR>α : Type u<VAR>f : Ultrafilter α<GOAL>IsAtom ↑f
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<GOAL>s ∈ ↑f ↔ s ∈ f
<VAR>α : Type u<GOAL>Function.Injective Ultrafilter.toFilter
<VAR>α : Type u<VAR>f g : Ultrafilter α<VAR>h : ↑f ≤ ↑g<GOAL>f = g
<VAR>α : Type u<VAR>f g : Ultrafilter α<GOAL>↑f ≤ ↑g ↔ f = g
<VAR>α : Type u<VAR>f g : Ultrafilter α<GOAL>↑f = ↑g ↔ f = g
<VAR>α : Type u<VAR>f g : Ultrafilter α<VAR>h : ∀ (s : Set α), s ∈ f ↔ s ∈ g<GOAL>f = g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>g : Filter α<VAR>hg : (↑f ⊓ g).NeBot<GOAL>↑f ≤ g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>g : Filter α<VAR>hg : (g ⊓ ↑f).NeBot<GOAL>↑f ≤ g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>g : Filter α<GOAL>(↑f ⊓ g).NeBot ↔ ↑f ≤ g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>g : Filter α<GOAL>Disjoint (↑f) g ↔ ¬↑f ≤ g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<GOAL>sᶜ ∉ f ↔ s ∈ f
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in ↑f, p x) ↔ ∀ᶠ (x : α) in ↑f, p x
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<GOAL>sᶜ ∈ f ↔ s ∉ f
<VAR>α : Type u<VAR>s t : Set α<VAR>f : Ultrafilter α<GOAL>s \ t ∈ f ↔ s ∈ f ∧ t ∉ f
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>s.Nonempty
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>s ≠ ∅
<VAR>α : Type u<VAR>f : Ultrafilter α<GOAL>∅ ∉ f
<VAR>α : Type u<VAR>u : Ultrafilter α<VAR>f g : Filter α<GOAL>↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s t : Set α<GOAL>s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<GOAL>s ∈ f ∨ sᶜ ∈ f
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, ¬p x
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>p q : α → Prop<GOAL>(∀ᶠ (x : α) in ↑f, p x ∨ q x) ↔ (∀ᶠ (x : α) in ↑f, p x) ∨ ∀ᶠ (x : α) in ↑f, q x
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in ↑f, ¬p x) ↔ ¬∀ᶠ (x : α) in ↑f, p x
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>p q : α → Prop<GOAL>(∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set (Set α)<VAR>hs : s.Finite<GOAL>⋃₀ s ∈ f ↔ ∃ t ∈ s, t ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Ultrafilter α<VAR>is : Set β<VAR>s : β → Set α<VAR>his : is.Finite<GOAL>⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>f : Ultrafilter α<GOAL>↑(Ultrafilter.map m f) = Filter.map m ↑f
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>f : Ultrafilter α<VAR>s : Set β<GOAL>s ∈ Ultrafilter.map m f ↔ m ⁻¹' s ∈ f
<VAR>α : Type u<VAR>f : Ultrafilter α<GOAL>Ultrafilter.map id f = f
<VAR>α : Type u<VAR>f : Ultrafilter α<GOAL>Ultrafilter.map (fun x => x) f = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Ultrafilter α<VAR>m : α → β<VAR>n : β → γ<GOAL>Ultrafilter.map n (Ultrafilter.map m f) = Ultrafilter.map (n ∘ m) f
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>u : Ultrafilter β<VAR>inj : Function.Injective m<VAR>large : Set.range m ∈ u<VAR>s : Set α<GOAL>s ∈ u.comap inj large ↔ m '' s ∈ u
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>u : Ultrafilter β<VAR>inj : Function.Injective m<VAR>large : Set.range m ∈ u<GOAL>↑(u.comap inj large) = Filter.comap m ↑u
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>h₀ : Function.Injective id := ⋯<VAR>h₁ : Set.range id ∈ f := ⋯<GOAL>f.comap h₀ h₁ = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Ultrafilter γ<VAR>m : α → β<VAR>n : β → γ<VAR>inj₀ : Function.Injective n<VAR>large₀ : Set.range n ∈ f<VAR>inj₁ : Function.Injective m<VAR>large₁ : Set.range m ∈ f.comap inj₀ large₀<VAR>inj₂ : Function.Injective (n ∘ m) := ⋯<VAR>large₂ : Set.range (n ∘ m) ∈ f := ⋯<GOAL>(f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂
<VAR>α : Type u<VAR>a : α<VAR>s : Set α<GOAL>s ∈ pure a ↔ a ∈ s
<VAR>α : Type u<VAR>a : α<GOAL>↑(pure a) = pure a
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>a : α<GOAL>Ultrafilter.map m (pure a) = pure (m a)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>a : α<VAR>inj : Function.Injective m<VAR>large : Set.range m ∈ pure (m a)<GOAL>(pure (m a)).comap inj large = pure a
<VAR>α : Type u<VAR>f : Ultrafilter α<VAR>s : Set α<VAR>h : s.Finite<VAR>h' : s ∈ f<GOAL>∃ x ∈ s, f = pure x
<VAR>α : Type u<VAR>Finite α<VAR>f : Ultrafilter α<GOAL>∃ a, f = pure a
<VAR>α : Type u<VAR>f : Ultrafilter α<GOAL>↑f ≤ Filter.cofinite ∨ ∃ a, f = pure a
<VAR>α : Type u<VAR>f : Filter α<VAR>h : f.NeBot<GOAL>∃ u, ↑u ≤ f
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<GOAL>↑(Ultrafilter.of f) ≤ f
<VAR>α : Type u<VAR>f : Ultrafilter α<GOAL>Ultrafilter.of ↑f = f
<VAR>α : Type u<VAR>S : Set (Set α)<VAR>cond : ∀ (T : Finset (Set α)), ↑T ⊆ S → (⋂₀ ↑T).Nonempty<GOAL>∃ F, S ⊆ (↑F).sets
<VAR>α : Type u<VAR>a : α<GOAL>IsAtom (pure a)
<VAR>α : Type u<VAR>f : Filter α<VAR>a : α<VAR>hf : f.NeBot<GOAL>f ≤ pure a ↔ f = pure a
<VAR>α : Type u<VAR>f : Filter α<VAR>hf : f.NeBot<VAR>x : α<GOAL>f = pure x ↔ {x} ∈ f
<VAR>α : Type u<VAR>LinearOrder α<VAR>x : α<VAR>hx : IsTop x<GOAL>Filter.atTop = pure x
<VAR>α : Type u<VAR>LinearOrder α<VAR>x : α<VAR>hx : IsBot x<GOAL>Filter.atBot = pure x
<VAR>α : Type u<VAR>f : Filter α<VAR>a : α<GOAL>f < pure a ↔ f = ⊥
<VAR>α : Type u<VAR>f : Filter α<VAR>a : α<GOAL>f ≤ pure a ↔ f = ⊥ ∨ f = pure a
<VAR>α : Type u<VAR>a : α<GOAL>Set.Iic (pure a) = {⊥, pure a}
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<GOAL>s ∈ f ↔ ∀ (g : Ultrafilter α), ↑g ≤ f → s ∈ g
<VAR>α : Type u<VAR>f₁ f₂ : Filter α<GOAL>f₁ ≤ f₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ f₁ → ↑g ≤ f₂
<VAR>α : Type u<VAR>f : Filter α<GOAL>⨆ g, ⨆ (_ : ↑g ≤ f), ↑g = f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.Tendsto f l₁ l₂ ↔ ∀ (g : Ultrafilter α), ↑g ≤ l₁ → Filter.Tendsto f (↑g) l₂
<VAR>α : Type u<VAR>f : Filter α<GOAL>(∃ u, ↑u ≤ f) ↔ f.NeBot
<VAR>α : Type u<VAR>g : Filter α<VAR>p : Filter α → Prop<VAR>hp : Monotone p<GOAL>(∀ (f : Filter α), f.NeBot → f ≤ g → p f) ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f
<VAR>α : Type u<VAR>Infinite α<GOAL>↑(Filter.hyperfilter α) ≤ Filter.cofinite
<GOAL>↑(Filter.hyperfilter ℕ) ≤ Filter.atTop
<VAR>α : Type u<VAR>Infinite α<GOAL>⊥ ≠ ↑(Filter.hyperfilter α)
<VAR>α : Type u<VAR>Infinite α<VAR>s : Set α<VAR>hf : s.Finite<GOAL>s ∉ Filter.hyperfilter α
<VAR>α : Type u<VAR>Infinite α<VAR>s : Set α<VAR>hf : s.Finite<GOAL>sᶜ ∈ Filter.hyperfilter α
<VAR>α : Type u<VAR>Infinite α<VAR>s : Set α<VAR>hf : sᶜ.Finite<GOAL>s ∈ Filter.hyperfilter α
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<GOAL>(Filter.comap m ↑g ⊓ 𝓟 s).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<GOAL>s ∈ Ultrafilter.ofComapInfPrincipal h
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>s : Set α<VAR>g : Ultrafilter β<VAR>h : m '' s ∈ g<GOAL>Ultrafilter.map m (Ultrafilter.ofComapInfPrincipal h) = g
<VAR>α : Type u<VAR>self : GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ⊓ b ⊓ a \ b = ⊥
<VAR>α : Type u<VAR>self : GeneralizedBooleanAlgebra α<VAR>a b : α<GOAL>a ⊓ b ⊔ a \ b = a
<VAR>α : Type u<VAR>GeneralizedBooleanAlgebra α<VAR>x y : α<GOAL>x ⊓ y ⊔ x \ y = x
<VAR>α : Type u<VAR>GeneralizedBooleanAlgebra α<VAR>x y : α<GOAL>x ⊓ y ⊓ x \ y = ⊥
<VAR>α : Type u<VAR>GeneralizedBooleanAlgebra α<VAR>x y : α<GOAL>x \ y ⊔ x ⊓ y = x
<VAR>α : Type u<VAR>GeneralizedBooleanAlgebra α<VAR>x y : α<GOAL>x \ y ⊓ (x ⊓ y) = ⊥
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>Disjoint (x ⊓ y) (x \ y)
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>s : x ⊓ y ⊔ z = x<VAR>i : x ⊓ y ⊓ z = ⊥<GOAL>x \ y = z
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ y ≤ x
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>y \ x ⊔ x = y ⊔ x
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ y ⊓ y \ x = ⊥
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>Disjoint (x \ y) (y \ x)
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x ⊓ y \ x = ⊥
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>y \ x ⊓ x = ⊥
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>Disjoint (y \ x) x
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>Disjoint x (y \ x)
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ y = x ↔ Disjoint x y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hi : Disjoint x z<VAR>hs : x ⊔ z = y<GOAL>y \ x = z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hd : Disjoint x z<VAR>hz : z ≤ y<VAR>hs : y ≤ x ⊔ z<GOAL>y \ x = z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<GOAL>Disjoint z (y \ x) ↔ z ≤ x
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<GOAL>z ≤ x ↔ Disjoint z (y \ x)
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<GOAL>z ⊓ y \ x = ⊥ ↔ z ≤ x
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hz : z ≤ y<VAR>hx : x ≤ y<GOAL>x ≤ z ↔ y = z ⊔ y \ x
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>y \ (x ⊔ z) = y \ x ⊓ y \ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>y \ x = y \ z ↔ y ⊓ x = y ⊓ z
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ y = x ↔ Disjoint y x
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<VAR>hx : y ≤ x<VAR>hy : y ≠ ⊥<GOAL>x \ y < x
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x ≤ y \ x ↔ x = ⊥
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ y = y ↔ x = ⊥ ∧ y = ⊥
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>h : x < y<VAR>hz : z ≤ x<GOAL>x \ z < y \ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ (y \ z) = x \ y ⊔ x ⊓ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>h : z ≤ x<GOAL>x \ (y \ z) = x \ y ⊔ z
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ (x \ y) = x ⊓ y
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<VAR>h : y ≤ x<GOAL>x \ (x \ y) = y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hy : y ≤ x<VAR>h : x \ y = z<GOAL>x \ z = y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hy : y ≤ x<VAR>hz : z ≤ x<GOAL>x \ y = z ↔ x \ z = y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hxz : x ≤ z<VAR>hyz : y ≤ z<VAR>h : z \ x = z \ y<GOAL>x = y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>(x \ y) \ z = x \ y ⊓ x \ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hca : z ≤ x<GOAL>(x \ y) \ (x \ z) = z \ y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>hcb : z ≤ y<GOAL>(x \ z) \ (y \ z) = x \ y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>(x ⊓ y) \ z = x \ z ⊓ y \ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>(x ⊓ y) \ z = x ⊓ y \ z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x \ z ⊓ y = (x ⊓ y) \ z
<VAR>α : Type u<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
<VAR>α : Type u<VAR>GeneralizedBooleanAlgebra α<VAR>a b c : α<GOAL>a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<GOAL>Disjoint (x \ z) y ↔ Disjoint x (y \ z)
<VAR>α : Type u<VAR>x y : α<VAR>GeneralizedBooleanAlgebra α<GOAL>x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>h : y < z \ x<VAR>hxz : x ≤ z<GOAL>x ⊔ y < z
<VAR>α : Type u<VAR>x y z : α<VAR>GeneralizedBooleanAlgebra α<VAR>h : x < z \ y<VAR>hyz : y ≤ z<GOAL>x ⊔ y < z
<VAR>α : Type u<VAR>self : BooleanAlgebra α<VAR>x : α<GOAL>x ⊓ xᶜ ≤ ⊥
<VAR>α : Type u<VAR>self : BooleanAlgebra α<VAR>x y : α<GOAL>x ⇨ y = y ⊔ xᶜ
<VAR>α : Type u<VAR>self : BooleanAlgebra α<VAR>x y : α<GOAL>x \ y = x ⊓ yᶜ
<VAR>α : Type u<VAR>self : BooleanAlgebra α<VAR>a : α<GOAL>a ≤ ⊤
<VAR>α : Type u<VAR>self : BooleanAlgebra α<VAR>a : α<GOAL>⊥ ≤ a
<VAR>α : Type u<VAR>self : BooleanAlgebra α<VAR>x : α<GOAL>⊤ ≤ x ⊔ xᶜ
<VAR>α : Type u<VAR>x : α<VAR>BooleanAlgebra α<GOAL>x ⊓ xᶜ = ⊥