ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>l : Filter α<VAR>f g h : α → β<VAR>hf : f ≤ᶠ[l] h<VAR>hg : g ≤ᶠ[l] h<GOAL>f ⊔ g ≤ᶠ[l] h
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>l : Filter α<VAR>f g h : α → β<VAR>hf : h ≤ᶠ[l] f<GOAL>h ≤ᶠ[l] f ⊔ g
<VAR>α : Type u<VAR>β : Type v<VAR>SemilatticeSup β<VAR>l : Filter α<VAR>f g h : α → β<VAR>hg : h ≤ᶠ[l] g<GOAL>h ≤ᶠ[l] f ⊔ g
<VAR>α : Type u<VAR>f : Filter (Filter α)<VAR>l : Filter α<VAR>h : ∀ᶠ (m : Filter α) in f, m ≤ l<GOAL>f.join ≤ l
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<GOAL>Filter.map f (𝓟 s) = 𝓟 (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>P : β → Prop<GOAL>(∀ᶠ (b : β) in Filter.map m f, P b) ↔ ∀ᶠ (a : α) in f, P (m a)
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>P : β → Prop<GOAL>(∃ᶠ (b : β) in Filter.map m f, P b) ↔ ∃ᶠ (a : α) in f, P (m a)
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>t : Set β<GOAL>t ∈ Filter.map m f ↔ m ⁻¹' t ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>t : Set β<GOAL>t ∈ Filter.map m f ↔ {x | m x ∈ t} ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>s : Set α<VAR>hs : s ∈ f<GOAL>m '' s ∈ Filter.map m f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>s : Set α<VAR>hf : Function.Injective m<GOAL>m '' s ∈ Filter.map m f ↔ s ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<GOAL>Set.range m ∈ Filter.map m f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>t : Set β<GOAL>t ∈ Filter.map m f ↔ ∃ s ∈ f, m '' s ⊆ t
<VAR>α : Type u<VAR>f : Filter α<GOAL>Filter.map id f = f
<VAR>α : Type u<VAR>f : Filter α<GOAL>Filter.map (fun x => x) f = f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>m : α → β<VAR>m' : β → γ<GOAL>Filter.map m' ∘ Filter.map m = Filter.map (m' ∘ m)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Filter α<VAR>m : α → β<VAR>m' : β → γ<GOAL>Filter.map m' (Filter.map m f) = Filter.map (m' ∘ m) f
<VAR>α : Type u<VAR>β : Type v<VAR>m₁ m₂ : α → β<VAR>f : Filter α<VAR>h : m₁ =ᶠ[f] m₂<GOAL>Filter.map m₁ f = Filter.map m₂ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<VAR>s : Set α<GOAL>s ∈ Filter.comap f l ↔ {y | ∀ ⦃x : α⦄, f x = y → x ∈ s} ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<VAR>s : Set α<GOAL>s ∈ Filter.comap f l ↔ Set.kernImage f s ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>s : Set β<VAR>F : Filter (α × β)<GOAL>s ∈ Filter.comap (Prod.mk x) F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<VAR>p : α → Prop<GOAL>(∀ᶠ (a : α) in Filter.comap f l, p a) ↔ ∀ᶠ (b : β) in l, ∀ (a : α), f a = b → p a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<VAR>p : α → Prop<GOAL>(∃ᶠ (a : α) in Filter.comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ a, f a = b ∧ p a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<VAR>s : Set α<GOAL>s ∈ Filter.comap f l ↔ (f '' sᶜ)ᶜ ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<VAR>s : Set α<GOAL>sᶜ ∈ Filter.comap f l ↔ (f '' s)ᶜ ∈ l
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<GOAL>s ∈ Filter.kernMap m f ↔ ∃ t ∈ f, Set.kernImage m t = s
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<GOAL>s ∈ Filter.kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = sᶜ
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>f : Filter α<VAR>s : Set β<GOAL>sᶜ ∈ Filter.kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s
<VAR>α : Type u<VAR>a : α<GOAL>(pure a).sets = {s | a ∈ s}
<VAR>α : Type u<VAR>a : α<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in pure a, p x) ↔ p a
<VAR>α : Type u<VAR>a : α<GOAL>𝓟 {a} = pure a
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>a : α<GOAL>Filter.map f (pure a) = pure (f a)
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<GOAL>pure a ≤ 𝓟 s ↔ a ∈ s
<VAR>α : Type u<VAR>f : Filter α<GOAL>(pure f).join = f
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>m : α → Filter β<GOAL>(pure a).bind m = m a
<VAR>γ : Type w<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m : β → γ<VAR>f : Filter α<VAR>g : α → Filter β<GOAL>Filter.map m (f.bind g) = f.bind (Filter.map m ∘ g)
<VAR>γ : Type w<VAR>α : Type u_2<VAR>β : Type u_3<VAR>m : α → β<VAR>f : Filter α<VAR>g : β → Filter γ<GOAL>(Filter.map m f).bind g = f.bind (g ∘ m)
<VAR>α β : Type u_2<VAR>m : α → β<VAR>f : Filter α<GOAL>m <$> f = Filter.map m f
<VAR>α β : Type u_2<VAR>f : Filter α<VAR>m : α → Filter β<GOAL>f >>= m = f.bind m
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>m : α → β<VAR>s : Set α<GOAL>s ∈ Filter.comap m g ↔ ∃ t ∈ g, m ⁻¹' t ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>m : α → β<VAR>t : Set β<VAR>ht : t ∈ g<GOAL>m ⁻¹' t ∈ Filter.comap m g
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>p : β → Prop<VAR>hf : ∀ᶠ (b : β) in g, p b<VAR>f : α → β<GOAL>∀ᶠ (a : α) in Filter.comap f g, p (f a)
<VAR>α : Type u<VAR>f : Filter α<GOAL>Filter.comap id f = f
<VAR>α : Type u<VAR>f : Filter α<GOAL>Filter.comap (fun x => x) f = f
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>t : Set β<VAR>x : β<VAR>ht : t ∈ g<VAR>hx : x ∉ t<GOAL>Filter.comap (fun x_1 => x) g = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>x : β<VAR>h : ∀ t ∈ g, x ∈ t<GOAL>Filter.comap (fun x_1 => x) g = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>f.NeBot<VAR>c : β<GOAL>Filter.map (fun x => c) f = pure c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Filter α<VAR>m : γ → β<VAR>n : β → α<GOAL>Filter.comap m (Filter.comap n f) = Filter.comap (n ∘ m) f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>φ : α → β<VAR>θ : α → γ<VAR>ψ : β → δ<VAR>ρ : γ → δ<VAR>H : ψ ∘ φ = ρ ∘ θ<VAR>F : Filter α<GOAL>Filter.map ψ (Filter.map φ F) = Filter.map ρ (Filter.map θ F)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>φ : α → β<VAR>θ : α → γ<VAR>ψ : β → δ<VAR>ρ : γ → δ<VAR>H : ψ ∘ φ = ρ ∘ θ<VAR>G : Filter δ<GOAL>Filter.comap φ (Filter.comap ψ G) = Filter.comap θ (Filter.comap ρ G)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<GOAL>Function.Semiconj (Filter.map f) (Filter.map ga) (Filter.map gb)
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Commute (Filter.map f) (Filter.map g)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<GOAL>Function.Semiconj (Filter.comap f) (Filter.comap gb) (Filter.comap ga)
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Commute (Filter.comap f) (Filter.comap g)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Function.LeftInverse g f<GOAL>Function.LeftInverse (Filter.map g) (Filter.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Function.LeftInverse g f<GOAL>Function.RightInverse (Filter.comap g) (Filter.comap f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Function.RightInverse g f<GOAL>Function.RightInverse (Filter.map g) (Filter.map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Function.RightInverse g f<GOAL>Function.LeftInverse (Filter.comap g) (Filter.comap f)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Set.LeftInvOn g f s<GOAL>Set.LeftInvOn (Filter.map g) (Filter.map f) (Set.Iic (𝓟 s))
<VAR>α : Type u<VAR>β : Type v<VAR>t : Set β<VAR>f : α → β<VAR>g : β → α<VAR>hfg : Set.RightInvOn g f t<GOAL>Set.RightInvOn (Filter.map g) (Filter.map f) (Set.Iic (𝓟 t))
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>t : Set β<GOAL>Filter.comap m (𝓟 t) = 𝓟 (m ⁻¹' t)
<VAR>α : Type u_2<VAR>s : Set α<VAR>t : Set ↑s<GOAL>𝓟 t = Filter.comap Subtype.val (𝓟 (Subtype.val '' t))
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>b : β<GOAL>Filter.comap m (pure b) = 𝓟 (m ⁻¹' {b})
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → β<GOAL>Filter.map m f ≤ g ↔ f ≤ Filter.comap m g
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>GaloisConnection (Filter.map m) (Filter.comap m)
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → β<GOAL>Filter.comap m g ≤ f ↔ g ≤ Filter.kernMap m f
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>GaloisConnection (Filter.comap m) (Filter.kernMap m)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>s : Set α<GOAL>Filter.kernMap m (𝓟 s) = 𝓟 (Set.kernImage m s)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>Monotone (Filter.map m)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>Monotone (Filter.comap m)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>F G : Filter α<VAR>h : F ≤ G<GOAL>Filter.map m F ≤ Filter.map m G
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>F G : Filter β<VAR>h : F ≤ G<GOAL>Filter.comap m F ≤ Filter.comap m G
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>Filter.map m ⊥ = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : Filter α<VAR>m : α → β<GOAL>Filter.map m (f₁ ⊔ f₂) = Filter.map m f₁ ⊔ Filter.map m f₂
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>m : α → β<VAR>f : ι → Filter α<GOAL>Filter.map m (⨆ i, f i) = ⨆ i, Filter.map m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>Filter.map f ⊤ = 𝓟 (Set.range f)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>Filter.comap m ⊤ = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>g₁ g₂ : Filter β<VAR>m : α → β<GOAL>Filter.comap m (g₁ ⊓ g₂) = Filter.comap m g₁ ⊓ Filter.comap m g₂
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>m : α → β<VAR>f : ι → Filter β<GOAL>Filter.comap m (⨅ i, f i) = ⨅ i, Filter.comap m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter α<GOAL>l ≤ Filter.comap f ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>m : α → β<GOAL>Filter.map m (Filter.comap m g) ≤ g
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<GOAL>f ≤ Filter.comap m (Filter.map m f)
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<GOAL>Filter.comap m ⊥ = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>m : α → β<VAR>h : (Filter.comap m g).NeBot<GOAL>g.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>g : Filter β<VAR>m : α → β<GOAL>Filter.comap m (g ⊓ 𝓟 (Set.range m)) = Filter.comap m g
<VAR>α : Type u<VAR>β : Type v<VAR>g₁ g₂ : Filter β<VAR>m : α → β<VAR>h : Disjoint g₁ g₂<GOAL>Disjoint (Filter.comap m g₁) (Filter.comap m g₂)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort u_2<VAR>f : ι → Filter β<VAR>m : α → β<GOAL>Filter.comap m (iSup f) = ⨆ i, Filter.comap m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set (Filter β)<VAR>m : α → β<GOAL>Filter.comap m (sSup s) = ⨆ f ∈ s, Filter.comap m f
<VAR>α : Type u<VAR>β : Type v<VAR>g₁ g₂ : Filter β<VAR>m : α → β<GOAL>Filter.comap m (g₁ ⊔ g₂) = Filter.comap m g₁ ⊔ Filter.comap m g₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<GOAL>Filter.map m (Filter.comap m f) = f ⊓ 𝓟 (Set.range m)
<VAR>β : Type v<VAR>f : Filter β<VAR>s : Set β<GOAL>Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ 𝓟 s
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>hf : Set.range m ∈ f<GOAL>Filter.map m (Filter.comap m f) = f
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter β<VAR>m : α → β<VAR>hf : Set.range m ∈ f<GOAL>Filter.comap m f ≤ Filter.comap m g ↔ f ≤ g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>l : Filter β<GOAL>Filter.map f (Filter.comap f l) = l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Injective (Filter.comap f)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Filter.map f ⊤ = ⊤
<VAR>α : Type u<VAR>s : Set α<VAR>f : Filter α<GOAL>Filter.map Subtype.val (Filter.comap Subtype.val f) = f ⊓ 𝓟 s
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>c : β → α<VAR>h : Set.range c ∈ f<VAR>W : Set β<VAR>W_in : W ∈ Filter.comap c f<GOAL>c '' W ∈ f
<VAR>α : Type u<VAR>f : Filter α<VAR>U : Set α<VAR>h : U ∈ f<VAR>W : Set ↑U<VAR>W_in : W ∈ Filter.comap Subtype.val f<GOAL>Subtype.val '' W ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>h : Function.Injective m<GOAL>Filter.comap m (Filter.map m f) = f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>inj : Function.Injective m<VAR>large : Set.range m ∈ f<VAR>S : Set α<GOAL>S ∈ Filter.comap m f ↔ m '' S ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ l₂ : Filter α<VAR>f : α → β<VAR>s : Set α<VAR>h₁ : s ∈ l₁<VAR>h₂ : s ∈ l₂<VAR>hinj : Set.InjOn f s<GOAL>Filter.map f l₁ ≤ Filter.map f l₂ ↔ l₁ ≤ l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>m : α → β<VAR>hm : Function.Injective m<GOAL>Filter.map m f ≤ Filter.map m g ↔ f ≤ g
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>m : α → β<VAR>s : Set α<VAR>hsf : s ∈ f<VAR>hsg : s ∈ g<VAR>hm : Set.InjOn m s<GOAL>Filter.map m f = Filter.map m g ↔ f = g
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>m : α → β<VAR>hm : Function.Injective m<GOAL>Filter.map m f = Filter.map m g ↔ f = g
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>hm : Function.Injective m<GOAL>Function.Injective (Filter.map m)
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<GOAL>(Filter.comap m f).NeBot ↔ ∀ t ∈ f, ∃ a, m a ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>hm : ∀ t ∈ f, ∃ a, m a ∈ t<GOAL>(Filter.comap m f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<GOAL>(Filter.comap m f).NeBot ↔ ∃ᶠ (y : β) in f, y ∈ Set.range m
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<GOAL>(Filter.comap m f).NeBot ↔ (Set.range m)ᶜ ∉ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<GOAL>Filter.comap m f = ⊥ ↔ (Set.range m)ᶜ ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>hm : Function.Surjective m<GOAL>Filter.comap m f = ⊥ ↔ f = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>g₁ g₂ : Filter β<VAR>m : α → β<VAR>h : Function.Surjective m<GOAL>Disjoint (Filter.comap m g₁) (Filter.comap m g₂) ↔ Disjoint g₁ g₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<GOAL>f.NeBot → Set.range m ∈ f → (Filter.comap m f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<GOAL>(Filter.comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
<VAR>α : Type u<VAR>β : Type v<VAR>Nonempty β<VAR>f : Filter α<VAR>f.NeBot<GOAL>(Filter.comap Prod.fst f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<GOAL>(Filter.comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>Nonempty α<VAR>f : Filter β<VAR>f.NeBot<GOAL>(Filter.comap Prod.snd f).NeBot
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>i : ι<VAR>f : Filter (α i)<GOAL>(Filter.comap (Function.eval i) f).NeBot ↔ (∀ (j : ι), Nonempty (α j)) ∧ f.NeBot
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>∀ (j : ι), Nonempty (α j)<VAR>i : ι<VAR>f : Filter (α i)<GOAL>(Filter.comap (Function.eval i) f).NeBot ↔ f.NeBot
<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>∀ (j : ι), Nonempty (α j)<VAR>i : ι<VAR>f : Filter (α i)<VAR>f.NeBot<GOAL>(Filter.comap (Function.eval i) f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : m '' s ∈ f<GOAL>(Filter.comap m f ⊓ 𝓟 s).NeBot
<VAR>γ : Type w<VAR>s : Set γ<VAR>l : Filter γ<VAR>h : l.NeBot<VAR>h' : l ≤ 𝓟 s<GOAL>(Filter.comap Subtype.val l).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>hm : Function.Surjective m<GOAL>(Filter.comap m f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter β<VAR>m : α → β<VAR>hf : f.NeBot<VAR>s : Set α<VAR>hs : m '' s ∈ f<GOAL>(Filter.comap m f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<GOAL>Filter.map m f = ⊥ ↔ f = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>F : Filter α<GOAL>(Filter.map f F).NeBot ↔ F.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>hf : f.NeBot<VAR>m : α → β<GOAL>(Filter.map m f).NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<GOAL>(Filter.map m f).NeBot → f.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>F : Filter β<GOAL>⋂₀ (Filter.comap f F).sets = ⋂ U ∈ F, f ⁻¹' U
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>m : α → β<GOAL>Filter.map m (iInf f) ≤ ⨅ i, Filter.map m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort x<VAR>f : ι → Filter α<VAR>m : α → β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<VAR>Nonempty ι<GOAL>Filter.map m (iInf f) = ⨅ i, Filter.map m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type w<VAR>f : ι → Filter α<VAR>m : α → β<VAR>p : ι → Prop<VAR>h : DirectedOn (f ⁻¹'o fun x x_1 => x ≥ x_1) {x | p x}<VAR>ne : ∃ i, p i<GOAL>Filter.map m (⨅ i, ⨅ (_ : p i), f i) = ⨅ i, ⨅ (_ : p i), Filter.map m (f i)
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>m : α → β<GOAL>Filter.map m (f ⊓ g) ≤ Filter.map m f ⊓ Filter.map m g
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>m : α → β<VAR>h : Function.Injective m<GOAL>Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>m : α → β<VAR>t : Set α<VAR>htf : t ∈ f<VAR>htg : t ∈ g<VAR>h : Set.InjOn m t<GOAL>Filter.map m (f ⊓ g) = Filter.map m f ⊓ Filter.map m g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F G : Filter α<VAR>f : α → β<VAR>h : Disjoint (Filter.map f F) (Filter.map f G)<GOAL>Disjoint F G
<VAR>α : Type u<VAR>β : Type v<VAR>m : α → β<VAR>hm : Function.Injective m<VAR>f₁ f₂ : Filter α<GOAL>Disjoint (Filter.map m f₁) (Filter.map m f₂) ↔ Disjoint f₁ f₂
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>f : Filter β<GOAL>Filter.map (⇑e.symm) f = Filter.comap (⇑e) f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>n : β → α<VAR>h₁ : m ∘ n = id<VAR>h₂ : n ∘ m = id<GOAL>Filter.map m f = Filter.comap n f
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<VAR>f : Filter α<GOAL>Filter.comap (⇑e.symm) f = Filter.map (⇑e) f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter (α × β)<GOAL>Prod.swap <$> f = Filter.comap Prod.swap f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>f : Filter ((α × β) × γ × δ)<GOAL>Filter.map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f = Filter.comap (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>g : Filter β<VAR>h : ∀ s ∈ f, m '' s ∈ g<GOAL>g ≤ Filter.map m f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → β<VAR>g : Filter β<GOAL>g ≤ Filter.map m f ↔ ∀ s ∈ f, m '' s ∈ g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter β<GOAL>Filter.map f (F ⊓ Filter.comap f G) = Filter.map f F ⊓ G
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>F : Filter α<VAR>G : Filter β<GOAL>Filter.map f (Filter.comap f G ⊓ F) = G ⊓ Filter.map f F
<VAR>α : Type u<VAR>s : Set α<GOAL>𝓟 s = Filter.map Subtype.val ⊤
<VAR>α : Type u<VAR>F : Filter α<VAR>s : Set α<GOAL>F ⊓ 𝓟 s = ⊥ ↔ Filter.comap Subtype.val F = ⊥
<VAR>α : Type u<VAR>a : α<GOAL>{a} ∈ pure a
<VAR>α : Type u<VAR>f : Filter α<VAR>a : α<GOAL>f ≤ pure a ↔ {a} ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter (α → β)<VAR>g : Filter α<VAR>s : Set β<GOAL>s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, x y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter (α → β)<VAR>g : Filter α<VAR>s : Set β<GOAL>s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, u.seq t ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Filter α<VAR>g : Filter β<VAR>m : α → β → γ<VAR>s : Set γ<GOAL>s ∈ (Filter.map m f).seq g ↔ ∃ t u, t ∈ g ∧ u ∈ f ∧ ∀ x ∈ u, ∀ y ∈ t, m x y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter (α → β)<VAR>g : Filter α<VAR>s : Set (α → β)<VAR>t : Set α<VAR>hs : s ∈ f<VAR>ht : t ∈ g<GOAL>s.seq t ∈ f.seq g
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter (α → β)<VAR>g : Filter α<VAR>h : Filter β<VAR>hh : ∀ t ∈ f, ∀ u ∈ g, t.seq u ∈ h<GOAL>h ≤ f.seq g
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : Filter (α → β)<VAR>g₁ g₂ : Filter α<VAR>hf : f₁ ≤ f₂<VAR>hg : g₁ ≤ g₂<GOAL>f₁.seq g₁ ≤ f₂.seq g₂
<VAR>α : Type u<VAR>β : Type v<VAR>g : α → β<VAR>f : Filter α<GOAL>(pure g).seq f = Filter.map g f
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter (α → β)<VAR>a : α<GOAL>f.seq (pure a) = Filter.map (fun g => g a) f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x : Filter α<VAR>g : Filter (α → β)<VAR>h : Filter (β → γ)<GOAL>h.seq (g.seq x) = ((Filter.map (fun x x_1 => x ∘ x_1) h).seq g).seq x
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : Filter β<GOAL>(Filter.map Prod.mk f).seq g = (Filter.map (fun b a => (a, b)) g).seq f
<VAR>α β : Type u<VAR>f : Filter (α → β)<VAR>g : Filter α<GOAL>(Seq.seq f fun x => g) = f.seq g
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>m : α → Filter β<VAR>p : β → Prop<GOAL>(∀ᶠ (y : β) in f.bind m, p y) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Filter α<VAR>m : α → Filter β<VAR>g₁ g₂ : β → γ<GOAL>g₁ =ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>LE γ<VAR>f : Filter α<VAR>m : α → Filter β<VAR>g₁ g₂ : β → γ<GOAL>g₁ ≤ᶠ[f.bind m] g₂ ↔ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set β<VAR>f : Filter α<VAR>m : α → Filter β<GOAL>s ∈ f.bind m ↔ {a | s ∈ m a} ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set β<VAR>f : Filter α<VAR>m : α → Filter β<GOAL>s ∈ f.bind m ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : α → Filter β<VAR>l : Filter β<VAR>h : ∀ᶠ (x : α) in f, g x ≤ l<GOAL>f.bind g ≤ l
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : Filter α<VAR>g₁ g₂ : α → Filter β<VAR>hf : f₁ ≤ f₂<VAR>hg : g₁ ≤ᶠ[f₁] g₂<GOAL>f₁.bind g₁ ≤ f₂.bind g₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : Filter α<VAR>g : α → Filter β<VAR>s : Set β<GOAL>(f.bind fun x => g x ⊓ 𝓟 s) = f.bind g ⊓ 𝓟 s
<VAR>α : Type u<VAR>β : Type v<VAR>f g : Filter α<VAR>h : α → Filter β<GOAL>(f ⊔ g).bind h = f.bind h ⊔ g.bind h
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → Filter β<GOAL>(𝓟 s).bind f = ⨆ x ∈ s, f x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f ⁻¹' s ∈ l₁
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.Tendsto f l₁ l₂ ↔ ∀ ⦃p : β → Prop⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.Tendsto f l₁ l₂ ↔ ∀ s ∈ l₂, ∀ᶠ (x : α) in l₁, f x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>s : Set β<VAR>hf : Filter.Tendsto f l₁ l₂<VAR>h : s ∈ l₂<GOAL>∀ᶠ (x : α) in l₁, f x ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>p : β → Prop<VAR>hf : Filter.Tendsto f l₁ l₂<VAR>h : ∀ᶠ (y : β) in l₂, p y<GOAL>∀ᶠ (x : α) in l₁, p (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>¬Filter.Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>p : β → Prop<VAR>hf : Filter.Tendsto f l₁ l₂<VAR>h : ∃ᶠ (x : α) in l₁, p (f x)<GOAL>∃ᶠ (y : β) in l₂, p y
<VAR>α : Type u<VAR>β : Type v<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>p : α → Prop<VAR>q : β → Prop<VAR>f : α → β<VAR>c : Filter.Tendsto f l₁ l₂<VAR>w : ∀ (x : α), p x → q (f x)<VAR>h : ∃ᶠ (x : α) in l₁, p x<GOAL>∃ᶠ (y : β) in l₂, q y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter β<GOAL>Filter.Tendsto f ⊥ l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l : Filter α<GOAL>Filter.Tendsto f l ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>mab : α → β<VAR>mba : β → α<VAR>f : Filter α<VAR>g : Filter β<VAR>h₁ : mab ∘ mba =ᶠ[g] id<VAR>h₂ : Filter.Tendsto mba g f<GOAL>g ≤ Filter.map mab f
<VAR>α : Type u<VAR>β : Type v<VAR>IsEmpty α<VAR>f : α → β<VAR>la : Filter α<VAR>lb : Filter β<GOAL>Filter.Tendsto f la lb
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g₁ g₂ : β → α<VAR>fa : Filter α<VAR>fb : Filter β<VAR>hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x<VAR>hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y<VAR>htendsto : Filter.Tendsto g₂ fb fa<GOAL>g₁ =ᶠ[fb] g₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<GOAL>Filter.Tendsto f l₁ l₂ ↔ l₁ ≤ Filter.comap f l₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>la₁ la₂ : Filter α<VAR>lb₁ lb₂ : Filter β<VAR>h₁ : Filter.Tendsto f la₁ lb₁<VAR>hd : Disjoint lb₁ lb₂<VAR>h₂ : Filter.Tendsto f la₂ lb₂<GOAL>Disjoint la₁ la₂
<VAR>α : Type u<VAR>β : Type v<VAR>f₁ f₂ : α → β<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>hl : f₁ =ᶠ[l₁] f₂<GOAL>Filter.Tendsto f₁ l₁ l₂ ↔ Filter.Tendsto f₂ l₁ l₂