ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>s t : Set α<GOAL>𝓟 s ≤ 𝓟 t ↔ s ⊆ t
<VAR>α : Type u<VAR>s t : Set α<GOAL>𝓟 s = 𝓟 t ↔ s = t
<VAR>α : Type u<VAR>s : Set (Filter α)<GOAL>(𝓟 s).join = sSup s
<VAR>α : Type u<GOAL>𝓟 Set.univ = ⊤
<VAR>α : Type u<GOAL>𝓟 ∅ = ⊥
<VAR>α : Type u<VAR>S : Set (Set α)<GOAL>Filter.generate S = ⨅ s ∈ S, 𝓟 s
<VAR>α : Type u<VAR>f : Filter α<GOAL>∅ ∈ f ↔ f = ⊥
<VAR>α : Type u<VAR>f : Filter α<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>s.Nonempty
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<GOAL>∅ ∉ f
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<GOAL>Nonempty α
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<VAR>f.NeBot<VAR>h : s ∈ f<GOAL>sᶜ ∉ f
<VAR>α : Type u<VAR>IsEmpty α<VAR>f : Filter α<GOAL>f = ⊥
<VAR>α : Type u<VAR>f g : Filter α<GOAL>Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t
<VAR>α : Type u<VAR>f g : Filter α<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>hs : s ∈ f<VAR>ht : t ∈ g<GOAL>Disjoint f g
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<VAR>hf : f.NeBot<VAR>hs : s ∈ f<VAR>ht : t ∈ f<GOAL>¬Disjoint s t
<VAR>α : Type u<VAR>f g : Filter α<GOAL>f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅
<VAR>α : Type u<VAR>ι : Type u_2<VAR>Finite ι<VAR>l : ι → Filter α<VAR>hd : Pairwise (Disjoint on l)<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Disjoint on s)
<VAR>α : Type u<VAR>ι : Type u_2<VAR>l : ι → Filter α<VAR>t : Set ι<VAR>hd : t.PairwiseDisjoint l<VAR>ht : t.Finite<GOAL>∃ s, (∀ (i : ι), s i ∈ l i) ∧ t.PairwiseDisjoint s
<VAR>α : Type u<VAR>f : Filter α<VAR>hf : f.NeBot<GOAL>Nonempty α
<VAR>α : Type u<VAR>Subsingleton α<VAR>l : Filter α<VAR>l.NeBot<GOAL>l = ⊤
<VAR>α : Type u<VAR>f : Filter α<GOAL>(∀ s ∈ f, s.Nonempty) ↔ f.NeBot
<VAR>α : Type u<GOAL>Nontrivial (Filter α) ↔ Nonempty α
<VAR>α : Type u<VAR>S : Set (Filter α)<VAR>l : Filter α<VAR>h : ∀ {s : Set α}, s ∈ l ↔ ∃ f ∈ S, s ∈ f<GOAL>l = sInf S
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>l : Filter α<VAR>h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, s ∈ f i<GOAL>l = iInf f
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>p : ι → Prop<VAR>l : Filter α<VAR>h : ∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i<GOAL>l = ⨅ i, ⨅ (_ : p i), f i
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>ne : Nonempty ι<GOAL>(iInf f).sets = ⋃ i, (f i).sets
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>h : Directed (fun x x_1 => x ≥ x_1) f<VAR>Nonempty ι<VAR>s : Set α<GOAL>s ∈ iInf f ↔ ∃ i, s ∈ f i
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → Filter α<VAR>s : Set β<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s<VAR>ne : s.Nonempty<VAR>t : Set α<GOAL>t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → Filter α<VAR>s : Set β<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) s<VAR>ne : s.Nonempty<GOAL>(⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets
<VAR>α : Type u<VAR>ι : Type u_2<VAR>f : ι → Filter α<GOAL>(⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i).sets
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<GOAL>(⨅ i, f i).sets = ⋃ t, (⨅ i ∈ t, f i.down).sets
<VAR>α : Type u<VAR>ι : Type u_2<VAR>f : ι → Filter α<VAR>s : Set α<GOAL>s ∈ iInf f ↔ ∃ t, s ∈ ⨅ i ∈ t, f i
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>s : Set α<GOAL>s ∈ iInf f ↔ ∃ t, s ∈ ⨅ i ∈ t, f i.down
<VAR>α : Type u<VAR>f₁ f₂ : Filter (Filter α)<GOAL>f₁.join ⊔ f₂.join = (f₁ ⊔ f₂).join
<VAR>α : Type u<VAR>ι : Sort w<VAR>f : ι → Filter (Filter α)<GOAL>⨆ x, (f x).join = (⨆ x, f x).join
<VAR>α : Type u<VAR>β : Type v<VAR>s : Finset α<VAR>f : α → Filter β<VAR>t : Set β<GOAL>t ∈ ⨅ a ∈ s, f a ↔ ∃ p, (∀ a ∈ s, p a ∈ f a) ∧ t = ⋂ a ∈ s, p a
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>Nonempty ι<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<GOAL>(∀ (i : ι), (f i).NeBot) → (iInf f).NeBot
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>hn : Nonempty α<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<VAR>hb : ∀ (i : ι), (f i).NeBot<GOAL>(iInf f).NeBot
<VAR>α : Type u<VAR>s : Set (Filter α)<VAR>hne : s.Nonempty<VAR>hd : DirectedOn (fun x x_1 => x ≥ x_1) s<VAR>hbot : ⊥ ∉ s<GOAL>(sInf s).NeBot
<VAR>α : Type u<VAR>Nonempty α<VAR>s : Set (Filter α)<VAR>hd : DirectedOn (fun x x_1 => x ≥ x_1) s<VAR>hbot : ⊥ ∉ s<GOAL>(sInf s).NeBot
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>Nonempty ι<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<GOAL>(iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>Nonempty α<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<GOAL>(iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>s : Set α<VAR>hs : s ∈ iInf f<VAR>p : Set α → Prop<VAR>uni : p Set.univ<VAR>ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)<GOAL>p s
<VAR>α : Type u<VAR>s t : Set α<GOAL>𝓟 s ⊓ 𝓟 t = 𝓟 (s ∩ t)
<VAR>α : Type u<VAR>s t : Set α<GOAL>𝓟 s ⊔ 𝓟 t = 𝓟 (s ∪ t)
<VAR>α : Type u<VAR>ι : Sort w<VAR>s : ι → Set α<GOAL>⨆ x, 𝓟 (s x) = 𝓟 (⋃ i, s i)
<VAR>α : Type u<VAR>s : Set α<GOAL>𝓟 s = ⊥ ↔ s = ∅
<VAR>α : Type u<VAR>s : Set α<GOAL>(𝓟 s).NeBot ↔ s.Nonempty
<VAR>α : Type u<VAR>s : Set α<GOAL>IsCompl (𝓟 s) (𝓟 sᶜ)
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<GOAL>s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s t : Set α<GOAL>s ∈ f ⊓ 𝓟 t ↔ {x | x ∈ t → x ∈ s} ∈ f
<VAR>α : Type u<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>s : Set α<GOAL>⨆ i, f i ⊓ 𝓟 s = (⨆ i, f i) ⊓ 𝓟 s
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<GOAL>f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<VAR>h : f ⊓ 𝓟 sᶜ = ⊥<GOAL>s ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<VAR>hs : s ∈ f<VAR>t : Set α<GOAL>s \ t ∈ f ⊓ 𝓟 tᶜ
<VAR>α : Type u<VAR>s : Set α<VAR>f : Filter α<GOAL>𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V
<VAR>α : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>f : ι → Set α<GOAL>⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
<VAR>α : Type u<VAR>ι : Sort w<VAR>Finite ι<VAR>f : ι → Set α<GOAL>⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)
<VAR>α : Type u<VAR>ι : Type w<VAR>Finite ι<VAR>f : ι → Set α<GOAL>⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)
<VAR>α : Type u<VAR>ι : Type w<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f : ι → Set α<GOAL>⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
<VAR>α : Type u<VAR>f₁ f₂ : Filter (Filter α)<VAR>h : f₁ ≤ f₂<GOAL>f₁.join ≤ f₂.join
<VAR>α : Type u<VAR>f : Filter α<VAR>P : α → Prop<GOAL>(∀ᶠ (x : α) in f, P x) ↔ {x | P x} ∈ f
<VAR>α : Type u<VAR>s : Set α<VAR>l : Filter α<GOAL>(∀ᶠ (x : α) in l, x ∈ s) ↔ s ∈ l
<VAR>α : Type u<VAR>f₁ f₂ : Filter α<VAR>h : ∀ (p : α → Prop), (∀ᶠ (x : α) in f₁, p x) ↔ ∀ᶠ (x : α) in f₂, p x<GOAL>f₁ = f₂
<VAR>α : Type u<VAR>f₁ f₂ : Filter α<VAR>h : f₁ ≤ f₂<VAR>p : α → Prop<VAR>hp : ∀ᶠ (x : α) in f₂, p x<GOAL>∀ᶠ (x : α) in f₁, p x
<VAR>α : Type u<VAR>f : Filter α<VAR>P : α → Prop<VAR>U : Set α<VAR>hU : U ∈ f<VAR>h : ∀ x ∈ U, P x<GOAL>∀ᶠ (x : α) in f, P x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<GOAL>Filter.Eventually p f → Filter.Eventually q f → ∀ᶠ (x : α) in f, p x ∧ q x
<VAR>α : Type u<VAR>f : Filter α<GOAL>∀ᶠ (x : α) in f, True
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<VAR>hp : ∀ (x : α), p x<GOAL>∀ᶠ (x : α) in f, p x
<VAR>α : Type u<VAR>f : Filter α<GOAL>(∀ᶠ (x : α) in f, False) ↔ f = ⊥
<VAR>α : Type u<VAR>f : Filter α<VAR>t : f.NeBot<VAR>p : Prop<GOAL>(∀ᶠ (x : α) in f, p) ↔ p
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<GOAL>(∀ᶠ (x : α) in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<VAR>hp : ∀ᶠ (x : α) in f, p x<GOAL>∃ v ∈ f, ∀ y ∈ v, p y
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∀ᶠ (x : α) in f, p x<VAR>hq : ∀ᶠ (x : α) in f, p x → q x<GOAL>∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∀ᶠ (x : α) in f, p x<VAR>hq : ∀ (x : α), p x → q x<GOAL>∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>p : α → β → Prop<VAR>h : ∀ᶠ (x : α) in f, ∀ (y : β), p x y<VAR>y : β<GOAL>∀ᶠ (x : α) in f, p x y
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<GOAL>(∀ᶠ (x : α) in f, p x ∧ q x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>f : Filter α<VAR>p q : α → Prop<VAR>h' : ∀ᶠ (x : α) in f, p x<VAR>h : ∀ᶠ (x : α) in f, p x ↔ q x<GOAL>∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>f : Filter α<VAR>p q : α → Prop<VAR>h : ∀ᶠ (x : α) in f, p x ↔ q x<GOAL>(∀ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>ι : Sort u_2<VAR>Finite ι<VAR>l : Filter α<VAR>p : ι → α → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
<VAR>α : Type u<VAR>ι : Type u_2<VAR>I : Set ι<VAR>hI : I.Finite<VAR>l : Filter α<VAR>p : ι → α → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
<VAR>α : Type u<VAR>ι : Type u_2<VAR>I : Finset ι<VAR>l : Filter α<VAR>p : ι → α → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ i ∈ I, p i x) ↔ ∀ i ∈ I, ∀ᶠ (x : α) in l, p i x
<VAR>α : Type u<VAR>f : Filter α<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∀ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>f : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q
<VAR>α : Type u<VAR>f : Filter α<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>p : α → Prop<GOAL>∀ᶠ (x : α) in ⊥, p x
<VAR>α : Type u<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in ⊤, p x) ↔ ∀ (x : α), p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f g : Filter α<GOAL>(∀ᶠ (x : α) in f ⊔ g, p x) ↔ (∀ᶠ (x : α) in f, p x) ∧ ∀ᶠ (x : α) in g, p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>fs : Set (Filter α)<GOAL>(∀ᶠ (x : α) in sSup fs, p x) ↔ ∀ f ∈ fs, ∀ᶠ (x : α) in f, p x
<VAR>α : Type u<VAR>ι : Sort x<VAR>p : α → Prop<VAR>fs : ι → Filter α<GOAL>(∀ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x
<VAR>α : Type u<VAR>a : Set α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in 𝓟 a, p x) ↔ ∀ x ∈ a, p x
<VAR>α : Type u_2<VAR>f : Filter α<VAR>s : Set α<VAR>P : α → Prop<VAR>hP : ∀ᶠ (x : α) in f, P x<VAR>hf : 𝓟 s ≤ f<VAR>x : α<GOAL>x ∈ s → P x
<VAR>α : Type u<VAR>f g : Filter α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in f ⊓ g, p x) ↔ ∃ s ∈ f, ∃ t ∈ g, ∀ x ∈ s ∩ t, p x
<VAR>α : Type u<VAR>f : Filter α<VAR>p : α → Prop<VAR>s : Set α<GOAL>(∀ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, x ∈ s → p x
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<VAR>p : α → Prop<VAR>h : ∀ᶠ (x : α) in f, p x<GOAL>∃ᶠ (x : α) in f, p x
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<VAR>p : α → Prop<VAR>h : ∀ (x : α), p x<GOAL>∃ᶠ (x : α) in f, p x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<VAR>h : ∃ᶠ (x : α) in f, p x<VAR>hpq : ∀ᶠ (x : α) in f, p x → q x<GOAL>∃ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f g : Filter α<VAR>h : ∃ᶠ (x : α) in f, p x<VAR>hle : f ≤ g<GOAL>∃ᶠ (x : α) in g, p x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<VAR>h : ∃ᶠ (x : α) in f, p x<VAR>hpq : ∀ (x : α), p x → q x<GOAL>∃ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<VAR>hq : ∀ᶠ (x : α) in f, q x<GOAL>∃ᶠ (x : α) in f, p x ∧ q x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>f : Filter α<VAR>hp : ∀ᶠ (x : α) in f, p x<VAR>hq : ∃ᶠ (x : α) in f, q x<GOAL>∃ᶠ (x : α) in f, p x ∧ q x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<VAR>hp : ∃ᶠ (x : α) in f, p x<GOAL>∃ x, p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<VAR>f.NeBot<VAR>hp : ∀ᶠ (x : α) in f, p x<GOAL>∃ x, p x
<VAR>α : Type u<VAR>l : Filter α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot
<VAR>α : Type u<VAR>l : Filter α<VAR>s : Set α<GOAL>(∃ᶠ (x : α) in l, x ∈ s) ↔ (l ⊓ 𝓟 s).NeBot
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<GOAL>(∃ᶠ (x : α) in f, p x) ↔ ∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, p x ∧ q x
<VAR>α : Type u<VAR>f : Filter α<VAR>P : α → Prop<GOAL>(∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<GOAL>(¬∀ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, ¬p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f : Filter α<GOAL>(¬∃ᶠ (x : α) in f, p x) ↔ ∀ᶠ (x : α) in f, ¬p x
<VAR>α : Type u<VAR>f : Filter α<GOAL>(∃ᶠ (x : α) in f, True) ↔ f.NeBot
<VAR>α : Type u<VAR>f : Filter α<GOAL>¬∃ᶠ (x : α) in f, False
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<VAR>p : Prop<GOAL>(∃ᶠ (x : α) in f, p) ↔ p
<VAR>α : Type u<VAR>f : Filter α<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 : Filter α<VAR>f.NeBot<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∃ᶠ (x : α) in f, p x ∨ q) ↔ (∃ᶠ (x : α) in f, p x) ∨ q
<VAR>α : Type u<VAR>f : Filter α<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 : Filter α<VAR>f.NeBot<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in f, p → q x) ↔ p → ∃ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>f : Filter α<VAR>f.NeBot<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∃ᶠ (x : α) in f, p x → q) ↔ (∀ᶠ (x : α) in f, p x) → q
<VAR>α : Type u<VAR>f : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∀ᶠ (x : α) in f, p x → q) ↔ (∃ᶠ (x : α) in f, p x) → q
<VAR>α : Type u<VAR>f : Filter α<VAR>p : Prop<VAR>q : α → Prop<GOAL>(∃ᶠ (x : α) in f, p ∧ q x) ↔ p ∧ ∃ᶠ (x : α) in f, q x
<VAR>α : Type u<VAR>f : Filter α<VAR>p : α → Prop<VAR>q : Prop<GOAL>(∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q
<VAR>α : Type u<VAR>p : α → Prop<GOAL>¬∃ᶠ (x : α) in ⊥, p x
<VAR>α : Type u<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x
<VAR>α : Type u<VAR>a : Set α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in 𝓟 a, p x) ↔ ∃ x ∈ a, p x
<VAR>α : Type u<VAR>f : Filter α<VAR>s : Set α<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>f g : Filter α<GOAL>(∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x
<VAR>α : Type u<VAR>p : α → Prop<VAR>fs : Set (Filter α)<GOAL>(∃ᶠ (x : α) in sSup fs, p x) ↔ ∃ f ∈ fs, ∃ᶠ (x : α) in f, p x
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>fs : β → Filter α<GOAL>(∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x
<VAR>α : Type u<VAR>β : Type v<VAR>r : α → β → Prop<VAR>l : Filter α<VAR>l.NeBot<VAR>h : ∀ᶠ (x : α) in l, ∃ y, r x y<GOAL>∃ f, ∀ᶠ (x : α) in l, r x (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<GOAL>∀ᶠ (x : α) in l, f x = g x
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<VAR>p : α → β → Prop<VAR>hf : ∀ᶠ (x : α) in l, p x (f x)<GOAL>∀ᶠ (x : α) in l, p x (g x)
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<GOAL>s =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ s ↔ x ∈ t
<VAR>α : Type u<VAR>s : Set α<VAR>l : Filter α<GOAL>s =ᶠ[l] Set.univ ↔ s ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<GOAL>∃ s ∈ l, Set.EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g : α → β<VAR>s : Set α<VAR>hs : s ∈ l<VAR>h : Set.EqOn f g s<GOAL>f =ᶠ[l] g
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g : α → β<GOAL>f =ᶠ[l] g ↔ ∃ s ∈ l, Set.EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>l l' : Filter α<VAR>f g : α → β<VAR>h₁ : f =ᶠ[l] g<VAR>h₂ : l' ≤ l<GOAL>f =ᶠ[l'] g
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f : α → β<GOAL>f =ᶠ[l] f
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α → β<VAR>l : Filter α<VAR>H : f =ᶠ[l] g<GOAL>g =ᶠ[l] f
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g h : α → β<VAR>H₁ : f =ᶠ[l] g<VAR>H₂ : g =ᶠ[l] h<GOAL>f =ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g h : α → β<VAR>H : f =ᶠ[l] g<GOAL>f =ᶠ[l] h ↔ g =ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g h : α → β<VAR>H : g =ᶠ[l] h<GOAL>f =ᶠ[l] g ↔ f =ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : Filter α<VAR>f f' : α → β<VAR>hf : f =ᶠ[l] f'<VAR>g g' : α → γ<VAR>hg : g =ᶠ[l] g'<GOAL>(fun x => (f x, g x)) =ᶠ[l] fun x => (f' x, g' x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f g : α → β<VAR>l : Filter α<VAR>H : f =ᶠ[l] g<VAR>h : β → γ<GOAL>h ∘ f =ᶠ[l] h ∘ g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>f f' : α → β<VAR>g g' : α → γ<VAR>l : Filter α<VAR>Hf : f =ᶠ[l] f'<VAR>h : β → γ → δ<VAR>Hg : g =ᶠ[l] g'<GOAL>(fun x => h (f x) (g x)) =ᶠ[l] fun x => h (f' x) (g' x)
<VAR>α : Type u<VAR>β : Type v<VAR>Add β<VAR>f f' g g' : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<VAR>h' : f' =ᶠ[l] g'<GOAL>(fun x => f x + f' x) =ᶠ[l] fun x => g x + g' x
<VAR>α : Type u<VAR>β : Type v<VAR>Mul β<VAR>f f' g g' : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<VAR>h' : f' =ᶠ[l] g'<GOAL>(fun x => f x * f' x) =ᶠ[l] fun x => g x * g' x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_2<VAR>Pow β γ<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<VAR>c : γ<GOAL>(fun x => f x ^ c) =ᶠ[l] fun x => g x ^ c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_2<VAR>SMul γ β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<VAR>c : γ<GOAL>(fun x => c • f x) =ᶠ[l] fun x => c • g x
<VAR>α : Type u<VAR>β : Type v<VAR>Neg β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<GOAL>(fun x => -f x) =ᶠ[l] fun x => -g x
<VAR>α : Type u<VAR>β : Type v<VAR>Inv β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<GOAL>(fun x => (f x)⁻¹) =ᶠ[l] fun x => (g x)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>Sub β<VAR>f f' g g' : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<VAR>h' : f' =ᶠ[l] g'<GOAL>(fun x => f x - f' x) =ᶠ[l] fun x => g x - g' x
<VAR>α : Type u<VAR>β : Type v<VAR>Div β<VAR>f f' g g' : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<VAR>h' : f' =ᶠ[l] g'<GOAL>(fun x => f x / f' x) =ᶠ[l] fun x => g x / g' x
<VAR>α : Type u<VAR>β : Type v<VAR>𝕜 : Type u_2<VAR>VAdd 𝕜 β<VAR>l : Filter α<VAR>f f' : α → 𝕜<VAR>g g' : α → β<VAR>hf : f =ᶠ[l] f'<VAR>hg : g =ᶠ[l] g'<GOAL>(fun x => f x +ᵥ g x) =ᶠ[l] fun x => f' x +ᵥ g' x
<VAR>α : Type u<VAR>β : Type v<VAR>𝕜 : Type u_2<VAR>SMul 𝕜 β<VAR>l : Filter α<VAR>f f' : α → 𝕜<VAR>g g' : α → β<VAR>hf : f =ᶠ[l] f'<VAR>hg : g =ᶠ[l] g'<GOAL>(fun x => f x • g x) =ᶠ[l] fun x => f' x • g' x
<VAR>α : Type u<VAR>β : Type v<VAR>Sup β<VAR>l : Filter α<VAR>f f' g g' : α → β<VAR>hf : f =ᶠ[l] f'<VAR>hg : g =ᶠ[l] g'<GOAL>(fun x => f x ⊔ g x) =ᶠ[l] fun x => f' x ⊔ g' x
<VAR>α : Type u<VAR>β : Type v<VAR>Inf β<VAR>l : Filter α<VAR>f f' g g' : α → β<VAR>hf : f =ᶠ[l] f'<VAR>hg : g =ᶠ[l] g'<GOAL>(fun x => f x ⊓ g x) =ᶠ[l] fun x => f' x ⊓ g' x
<VAR>α : Type u<VAR>β : Type v<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<VAR>s : Set β<GOAL>f ⁻¹' s =ᶠ[l] g ⁻¹' s
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s =ᶠ[l] t<VAR>h' : s' =ᶠ[l] t'<GOAL>s ∩ s' =ᶠ[l] t ∩ t'
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s =ᶠ[l] t<VAR>h' : s' =ᶠ[l] t'<GOAL>s ∪ s' =ᶠ[l] t ∪ t'
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<VAR>h : s =ᶠ[l] t<GOAL>sᶜ =ᶠ[l] tᶜ
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s =ᶠ[l] t<VAR>h' : s' =ᶠ[l] t'<GOAL>s \ s' =ᶠ[l] t \ t'
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s =ᶠ[l] t<VAR>h' : s' =ᶠ[l] t'<GOAL>s ∆ s' =ᶠ[l] t ∆ t'
<VAR>α : Type u<VAR>s : Set α<VAR>l : Filter α<GOAL>s =ᶠ[l] ∅ ↔ ∀ᶠ (x : α) in l, x ∉ s
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<GOAL>s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<GOAL>s ∩ t =ᶠ[l] t ↔ ∀ᶠ (x : α) in l, x ∈ t → x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f g : α → β<GOAL>f =ᶠ[𝓟 s] g ↔ Set.EqOn f g s
<VAR>α : Type u<VAR>β : Type v<VAR>F : Filter α<VAR>s : Set α<VAR>f g : α → β<GOAL>f =ᶠ[F ⊓ 𝓟 s] g ↔ ∀ᶠ (x : α) in F, x ∈ s → f x = g x
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f g : α → β<VAR>l : Filter α<VAR>h : f =ᶠ[l] g<GOAL>f - g =ᶠ[l] 0
<VAR>α : Type u<VAR>β : Type v<VAR>AddGroup β<VAR>f g : α → β<VAR>l : Filter α<GOAL>f =ᶠ[l] g ↔ f - g =ᶠ[l] 0
<VAR>α : Type u<VAR>β : Type v<VAR>LE β<VAR>l : Filter α<VAR>f f' g g' : α → β<VAR>H : f ≤ᶠ[l] g<VAR>hf : f =ᶠ[l] f'<VAR>hg : g =ᶠ[l] g'<GOAL>f' ≤ᶠ[l] g'
<VAR>α : Type u<VAR>β : Type v<VAR>LE β<VAR>l : Filter α<VAR>f f' g g' : α → β<VAR>hf : f =ᶠ[l] f'<VAR>hg : g =ᶠ[l] g'<GOAL>f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g'
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f =ᶠ[l] g<GOAL>f ≤ᶠ[l] g
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>f : α → β<GOAL>f ≤ᶠ[l] f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>f g h : α → β<VAR>H₁ : f ≤ᶠ[l] g<VAR>H₂ : g ≤ᶠ[l] h<GOAL>f ≤ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>f g h : α → β<VAR>H₁ : f =ᶠ[l] g<VAR>H₂ : g ≤ᶠ[l] h<GOAL>f ≤ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>f g h : α → β<VAR>H₁ : f ≤ᶠ[l] g<VAR>H₂ : g =ᶠ[l] h<GOAL>f ≤ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>l : Filter α<VAR>f g : α → β<VAR>h₁ : f ≤ᶠ[l] g<VAR>h₂ : g ≤ᶠ[l] f<GOAL>f =ᶠ[l] g
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>l : Filter α<VAR>f g : α → β<GOAL>f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>l : Filter α<VAR>f g : α → β<VAR>h : f ≤ᶠ[l] g<GOAL>g ≤ᶠ[l] f ↔ g =ᶠ[l] f
<VAR>α : Type u<VAR>β : Type v<VAR>Preorder β<VAR>l : Filter α<VAR>f g : α → β<VAR>h : ∀ᶠ (x : α) in l, f x < g x<GOAL>∀ᶠ (x : α) in l, f x ≠ g x
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>OrderTop β<VAR>l : Filter α<VAR>f g : α → β<VAR>h : ∀ᶠ (x : α) in l, f x < g x<GOAL>∀ᶠ (x : α) in l, f x ≠ ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>OrderTop β<VAR>l : Filter α<VAR>f : α → β<VAR>h : ∀ᶠ (x : α) in l, f x ≠ ⊤<GOAL>∀ᶠ (x : α) in l, f x < ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>PartialOrder β<VAR>OrderTop β<VAR>l : Filter α<VAR>f : α → β<GOAL>(∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s ≤ᶠ[l] t<VAR>h' : s' ≤ᶠ[l] t'<GOAL>s ∩ s' ≤ᶠ[l] t ∩ t'
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s ≤ᶠ[l] t<VAR>h' : s' ≤ᶠ[l] t'<GOAL>s ∪ s' ≤ᶠ[l] t ∪ t'
<VAR>α : Type u<VAR>ι : Sort x<VAR>l : Filter α<VAR>Finite ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ≤ᶠ[l] t i<GOAL>⋃ i, s i ≤ᶠ[l] ⋃ i, t i
<VAR>α : Type u<VAR>ι : Sort x<VAR>l : Filter α<VAR>Finite ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i =ᶠ[l] t i<GOAL>⋃ i, s i =ᶠ[l] ⋃ i, t i
<VAR>α : Type u<VAR>ι : Sort x<VAR>l : Filter α<VAR>Finite ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i ≤ᶠ[l] t i<GOAL>⋂ i, s i ≤ᶠ[l] ⋂ i, t i
<VAR>α : Type u<VAR>ι : Sort x<VAR>l : Filter α<VAR>Finite ι<VAR>s t : ι → Set α<VAR>h : ∀ (i : ι), s i =ᶠ[l] t i<GOAL>⋂ i, s i =ᶠ[l] ⋂ i, t i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<GOAL>⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>heq : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<GOAL>⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>heq : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<GOAL>⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → Set α<VAR>heq : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<GOAL>⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
<VAR>α : Type u<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>f g : ι → Set α<VAR>heq : ∀ i ∈ s, f i =ᶠ[l] g i<GOAL>⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<VAR>h : s ≤ᶠ[l] t<GOAL>tᶜ ≤ᶠ[l] sᶜ
<VAR>α : Type u<VAR>s t s' t' : Set α<VAR>l : Filter α<VAR>h : s ≤ᶠ[l] t<VAR>h' : t' ≤ᶠ[l] s'<GOAL>s \ s' ≤ᶠ[l] t \ t'
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<GOAL>s ≤ᶠ[l] t ↔ t ∈ l ⊓ 𝓟 s
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<GOAL>s ≤ᶠ[l] t ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t
<VAR>α : Type u<VAR>s t : Set α<VAR>l : Filter α<GOAL>s =ᶠ[l] t ↔ l ⊓ 𝓟 s = l ⊓ 𝓟 t
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<GOAL>f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂