# Documentation

Mathlib.Order.Filter.Cofinite

# 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} :

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

Instances For
@[simp]
theorem Filter.mem_cofinite {α : Type u_2} {s : Set α} :
s Filter.cofinite
@[simp]
theorem Filter.eventually_cofinite {α : Type u_2} {p : αProp} :
(∀ᶠ (x : α) in Filter.cofinite, p x) Set.Finite {x | ¬p x}
theorem Filter.hasBasis_cofinite {α : Type u_2} :
Filter.HasBasis Filter.cofinite (fun s => ) compl
instance Filter.cofinite_neBot {α : Type u_2} [] :
Filter.NeBot Filter.cofinite
@[simp]
theorem Filter.cofinite_eq_bot_iff {α : Type u_2} :
Filter.cofinite =
@[simp]
theorem Filter.cofinite_eq_bot {α : Type u_2} [] :
Filter.cofinite =
theorem Filter.frequently_cofinite_iff_infinite {α : Type u_2} {p : αProp} :
(∃ᶠ (x : α) in Filter.cofinite, p x) Set.Infinite {x | p x}
theorem Set.Finite.compl_mem_cofinite {α : Type u_2} {s : Set α} (hs : ) :
s Filter.cofinite
theorem Set.Finite.eventually_cofinite_nmem {α : Type u_2} {s : Set α} (hs : ) :
∀ᶠ (x : α) in Filter.cofinite, ¬x s
theorem Finset.eventually_cofinite_nmem {α : Type u_2} (s : ) :
∀ᶠ (x : α) in Filter.cofinite, ¬x s
theorem Set.infinite_iff_frequently_cofinite {α : Type u_2} {s : Set α} :
∃ᶠ (x : α) in Filter.cofinite, x s
theorem Filter.eventually_cofinite_ne {α : Type u_2} (x : α) :
∀ᶠ (a : α) in Filter.cofinite, a x
theorem Filter.le_cofinite_iff_compl_singleton_mem {α : Type u_2} {l : } :
l Filter.cofinite ∀ (x : α), {x} l
theorem Filter.le_cofinite_iff_eventually_ne {α : Type u_2} {l : } :
l Filter.cofinite ∀ (x : α), ∀ᶠ (y : α) in l, y x
theorem Filter.atTop_le_cofinite {α : Type u_2} [] [] :
Filter.atTop Filter.cofinite

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

theorem Filter.comap_cofinite_le {α : Type u_2} {β : Type u_3} (f : αβ) :
Filter.comap f Filter.cofinite Filter.cofinite
theorem Filter.coprod_cofinite {α : Type u_2} {β : Type u_3} :
Filter.coprod Filter.cofinite Filter.cofinite = Filter.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} [] :
(Filter.coprodᵢ fun i => Filter.cofinite) = Filter.cofinite
@[simp]
theorem Filter.disjoint_cofinite_left {α : Type u_2} {l : } :
Disjoint Filter.cofinite l s, s l
@[simp]
theorem Filter.disjoint_cofinite_right {α : Type u_2} {l : } :
Disjoint l Filter.cofinite s, s l
theorem Filter.countable_compl_ker {α : Type u_2} {l : } (h : Filter.cofinite l) :

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 : } (h : Filter.Tendsto f Filter.cofinite l) :

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

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 : } :
(∃ᶠ (n : ) in Filter.atTop, p n) Set.Infinite {n | p n}
theorem Filter.Tendsto.exists_within_forall_le {α : Type u_4} {β : Type u_5} [] {s : Set α} (hs : ) {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) :
a₀, a₀ s ∀ (a : α), a sf a₀ f a
theorem Filter.Tendsto.exists_forall_le {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) :
a₀, ∀ (a : α), f a₀ f a
theorem Filter.Tendsto.exists_within_forall_ge {α : Type u_2} {β : Type u_3} [] {s : Set α} (hs : ) {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
a₀, a₀ s ∀ (a : α), a sf a f a₀
theorem Filter.Tendsto.exists_forall_ge {α : Type u_2} {β : Type u_3} [] [] {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
a₀, ∀ (a : α), f a f a₀
theorem Function.Surjective.le_map_cofinite {α : Type u_2} {β : Type u_3} {f : αβ} (hf : ) :
Filter.cofinite Filter.map f Filter.cofinite
theorem Function.Injective.tendsto_cofinite {α : Type u_2} {β : Type u_3} {f : αβ} (hf : ) :
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 Function.Injective.comap_cofinite_eq {α : Type u_2} {β : Type u_3} {f : αβ} (hf : ) :
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 : ) :
Filter.Tendsto f Filter.atTop Filter.atTop

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