Basic facts about filters

A filter is closed under binary intersections, so its members, ordered by inclusion, are codirected. Together with Mathlib's Filter.inhabitedMem, this lets the members of a filter index a colimit, for instance the neighbourhoods {U // U ∈ 𝓝ˢ A}ᵒᵈ of a set ordered by reverse inclusion.

Main results

• Filter.isCodirectedOrder_mem: the members of a filter are codirected under inclusion.
• Equiv.symm_comp_eventuallyEq_iff: the eventual form of Equiv.symm_comp_eq, which moves an equivalence to the other side of an eventual equality.

instance Filter.isCodirectedOrder_mem {α : Type u_1} (f : Filter α) : IsCodirectedOrder { s : Set α // s ∈ f }

The members of a filter are codirected under inclusion: the intersection of two members is a member contained in both.

theorem Equiv.symm_comp_eventuallyEq_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : β ≃ γ) {l : Filter α} {f : α → β} {g : α → γ} : ⇑e.symm ∘ g =ᶠ[l] f ↔ g =ᶠ[l] ⇑e ∘ f

The eventual form of Equiv.symm_comp_eq: e.symm ∘ g agrees with f along a filter exactly when g agrees with e ∘ f there.