The cofinite filter

In this file we define

Filter.cofinite: the filter of sets with finite complement

and prove its basic properties. In particular, we prove that for ℕ it is equal to Filter.atTop.

TODO

Define filters for other cardinalities of the complement.

def Filter.cofinite {α : Type u_2} : Filter α

The cofinite filter is the filter of subsets whose complements are finite.

@[simp]

theorem Filter.mem_cofinite {α : Type u_2} {s : Set α} : s ∈ cofinite ↔ sᶜ.Finite

@[simp]

theorem Filter.eventually_cofinite {α : Type u_2} {p : α → Prop} : (∀ᶠ (x : α) in cofinite, p x) ↔ {x : α | ¬p x}.Finite

theorem Filter.hasBasis_cofinite {α : Type u_2} : cofinite.HasBasis (fun (s : Set α) => s.Finite) compl

instance Filter.cofinite_neBot {α : Type u_2} [Infinite α] : cofinite.NeBot

@[simp]

theorem Filter.cofinite_eq_bot_iff {α : Type u_2} : cofinite = ⊥ ↔ Finite α

@[simp]

theorem Filter.cofinite_eq_bot {α : Type u_2} [Finite α] : cofinite = ⊥

theorem Filter.frequently_cofinite_iff_infinite {α : Type u_2} {p : α → Prop} : (∃ᶠ (x : α) in cofinite, p x) ↔ {x : α | p x}.Infinite

theorem Filter.frequently_cofinite_mem_iff_infinite {α : Type u_2} {s : Set α} : (∃ᶠ (x : α) in cofinite, x ∈ s) ↔ s.Infinite

theorem Set.Infinite.frequently_cofinite {α : Type u_2} {s : Set α} : s.Infinite → ∃ᶠ (x : α) in Filter.cofinite, x ∈ s

Alias of the reverse direction of Filter.frequently_cofinite_mem_iff_infinite.

@[simp]

theorem Filter.cofinite_inf_principal_neBot_iff {α : Type u_2} {s : Set α} : (cofinite ⊓ principal s).NeBot ↔ s.Infinite

theorem Set.Infinite.cofinite_inf_principal_neBot {α : Type u_2} {s : Set α} : s.Infinite → (Filter.cofinite ⊓ Filter.principal s).NeBot

Alias of the reverse direction of Filter.cofinite_inf_principal_neBot_iff.

theorem Set.Finite.compl_mem_cofinite {α : Type u_2} {s : Set α} (hs : s.Finite) : sᶜ ∈ Filter.cofinite

theorem Set.Finite.eventually_cofinite_notMem {α : Type u_2} {s : Set α} (hs : s.Finite) : ∀ᶠ (x : α) in Filter.cofinite, x ∉ s

@[deprecated Set.Finite.eventually_cofinite_notMem (since := "2025-05-24")]

theorem Set.Finite.eventually_cofinite_nmem {α : Type u_2} {s : Set α} (hs : s.Finite) : ∀ᶠ (x : α) in Filter.cofinite, x ∉ s

Alias of Set.Finite.eventually_cofinite_notMem.

theorem Finset.eventually_cofinite_notMem {α : Type u_2} (s : Finset α) : ∀ᶠ (x : α) in Filter.cofinite, x ∉ s

@[deprecated Finset.eventually_cofinite_notMem (since := "2025-05-24")]

theorem Finset.eventually_cofinite_nmem {α : Type u_2} (s : Finset α) : ∀ᶠ (x : α) in Filter.cofinite, x ∉ s

Alias of Finset.eventually_cofinite_notMem.

theorem Set.infinite_iff_frequently_cofinite {α : Type u_2} {s : Set α} : s.Infinite ↔ ∃ᶠ (x : α) in Filter.cofinite, x ∈ s

theorem Filter.eventually_cofinite_ne {α : Type u_2} (x : α) : ∀ᶠ (a : α) in cofinite, a ≠ x

theorem Filter.le_cofinite_iff_compl_singleton_mem {α : Type u_2} {l : Filter α} : l ≤ cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l

theorem Filter.le_cofinite_iff_eventually_ne {α : Type u_2} {l : Filter α} : l ≤ cofinite ↔ ∀ (x : α), ∀ᶠ (y : α) in l, y ≠ x

theorem Filter.atTop_le_cofinite {α : Type u_2} [Preorder α] [NoTopOrder α] : atTop ≤ cofinite

If α is a preorder with no top element, then atTop ≤ cofinite.

theorem Filter.atBot_le_cofinite {α : Type u_2} [Preorder α] [NoBotOrder α] : atBot ≤ cofinite

If α is a preorder with no bottom element, then atBot ≤ cofinite.

theorem Filter.comap_cofinite_le {α : Type u_2} {β : Type u_3} (f : α → β) : comap f cofinite ≤ cofinite

theorem Filter.coprod_cofinite {α : Type u_2} {β : Type u_3} : cofinite.coprod cofinite = cofinite

The coproduct of the cofinite filters on two types is the cofinite filter on their product.

theorem Filter.coprodᵢ_cofinite {ι : Type u_1} {α : ι → Type u_4} [Finite ι] : (Filter.coprodᵢ fun (i : ι) => cofinite) = cofinite

theorem Filter.disjoint_cofinite_left {α : Type u_2} {l : Filter α} : Disjoint cofinite l ↔ ∃ s ∈ l, s.Finite

theorem Filter.disjoint_cofinite_right {α : Type u_2} {l : Filter α} : Disjoint l cofinite ↔ ∃ s ∈ l, s.Finite

theorem Filter.countable_compl_ker {α : Type u_2} {l : Filter α} [l.IsCountablyGenerated] (h : cofinite ≤ l) : l.kerᶜ.Countable

If l ≥ Filter.cofinite is a countably generated filter, then l.ker is cocountable.

theorem Filter.Tendsto.countable_compl_preimage_ker {α : Type u_2} {β : Type u_3} {f : α → β} {l : Filter β} [l.IsCountablyGenerated] (h : Tendsto f cofinite l) : (f ⁻¹' l.ker)ᶜ.Countable

If f tends to a countably generated filter l along Filter.cofinite, then for all but countably many elements, f x ∈ l.ker.

theorem Filter.univ_pi_mem_pi {ι : Type u_1} {α : ι → Type u_4} {s : (i : ι) → Set (α i)} {l : (i : ι) → Filter (α i)} (h : ∀ (i : ι), s i ∈ l i) (hfin : ∀ᶠ (i : ι) in cofinite, s i = Set.univ) : Set.univ.pi s ∈ pi l

Given a collection of filters l i : Filter (α i) and sets s i ∈ l i, if all but finitely many of s i are the whole space, then their indexed product Set.pi Set.univ s belongs to the filter Filter.pi l.

theorem Filter.map_piMap_pi {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {f : (i : ι) → α i → β i} (hf : ∀ᶠ (i : ι) in cofinite, Function.Surjective (f i)) (l : (i : ι) → Filter (α i)) : map (Pi.map f) (pi l) = pi fun (i : ι) => map (f i) (l i)

Given a family of maps f i : α i → β i and a family of filters l i : Filter (α i), if all but finitely many of f i are surjective, then the indexed product of f is maps the indexed product of the filters l i to the indexed products of their pushforwards under individual f is.

See also map_piMap_pi_finite for the case of a finite index type.

theorem Filter.map_piMap_pi_finite {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [Finite ι] (f : (i : ι) → α i → β i) (l : (i : ι) → Filter (α i)) : map (Pi.map f) (pi l) = pi fun (i : ι) => map (f i) (l i)

Given finite families of maps f i : α i → β i and of filters l i : Filter (α i), the indexed product of f is maps the indexed product of the filters l i to the indexed products of their pushforwards under individual f is.

See also map_piMap_pi for a more general case.

theorem Set.Finite.cofinite_inf_principal_compl {α : Type u_2} {s : Set α} (hs : s.Finite) : Filter.cofinite ⊓ Filter.principal sᶜ = Filter.cofinite

theorem Set.Finite.cofinite_inf_principal_diff {α : Type u_2} {s t : Set α} (ht : t.Finite) : Filter.cofinite ⊓ Filter.principal (s \ t) = Filter.cofinite ⊓ Filter.principal s

theorem Nat.cofinite_eq_atTop : Filter.cofinite = Filter.atTop

For natural numbers the filters Filter.cofinite and Filter.atTop coincide.

theorem Nat.frequently_atTop_iff_infinite {p : ℕ → Prop} : (∃ᶠ (n : ℕ) in Filter.atTop, p n) ↔ {n : ℕ | p n}.Infinite

theorem Nat.eventually_pos : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < k

theorem Filter.Tendsto.exists_within_forall_le {α : Type u_4} {β : Type u_5} [LinearOrder β] {s : Set α} (hs : s.Nonempty) {f : α → β} (hf : Tendsto f cofinite atTop) : ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

theorem Filter.Tendsto.exists_forall_le {α : Type u_2} {β : Type u_3} [Nonempty α] [LinearOrder β] {f : α → β} (hf : Tendsto f cofinite atTop) : ∃ (a₀ : α), ∀ (a : α), f a₀ ≤ f a

theorem Filter.Tendsto.exists_within_forall_ge {α : Type u_2} {β : Type u_3} [LinearOrder β] {s : Set α} (hs : s.Nonempty) {f : α → β} (hf : Tendsto f cofinite atBot) : ∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀

theorem Filter.Tendsto.exists_forall_ge {α : Type u_2} {β : Type u_3} [Nonempty α] [LinearOrder β] {f : α → β} (hf : Tendsto f cofinite atBot) : ∃ (a₀ : α), ∀ (a : α), f a ≤ f a₀

theorem Function.Surjective.le_map_cofinite {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Surjective f) : Filter.cofinite ≤ Filter.map f Filter.cofinite

theorem Function.Injective.tendsto_cofinite {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Injective f) : Filter.Tendsto f Filter.cofinite Filter.cofinite

For an injective function f, inverse images of finite sets are finite. See also Filter.comap_cofinite_le and Function.Injective.comap_cofinite_eq.

theorem Filter.Tendsto.cofinite_of_finite_preimage_singleton {α : Type u_2} {β : Type u_3} {f : α → β} (hf : ∀ (b : β), Finite ↑(f ⁻¹' {b})) : Tendsto f cofinite cofinite

For a function with finite fibres, inverse images of finite sets are finite.

theorem Function.Injective.comap_cofinite_eq {α : Type u_2} {β : Type u_3} {f : α → β} (hf : Injective f) : Filter.comap f Filter.cofinite = Filter.cofinite

The pullback of the Filter.cofinite under an injective function is equal to Filter.cofinite. See also Filter.comap_cofinite_le and Function.Injective.tendsto_cofinite.

theorem Function.Injective.nat_tendsto_atTop {f : ℕ → ℕ} (hf : Injective f) : Filter.Tendsto f Filter.atTop Filter.atTop

An injective sequence f : ℕ → ℕ tends to infinity at infinity.