# 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.

Equations
Instances For
@[simp]
theorem Filter.mem_cofinite {α : Type u_2} {s : Set α} :
s Filter.cofinite s.Finite
@[simp]
theorem Filter.eventually_cofinite {α : Type u_2} {p : αProp} :
(∀ᶠ (x : α) in Filter.cofinite, p x) {x : α | ¬p x}.Finite
theorem Filter.hasBasis_cofinite {α : Type u_2} :
Filter.cofinite.HasBasis (fun (s : Set α) => s.Finite) compl
instance Filter.cofinite_neBot {α : Type u_2} [] :
Filter.cofinite.NeBot
Equations
• =
@[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) {x : α | p x}.Infinite
theorem Filter.frequently_cofinite_mem_iff_infinite {α : Type u_2} {s : Set α} :
(∃ᶠ (x : α) in Filter.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 α} :
(Filter.cofinite ).NeBot s.Infinite
theorem Set.Infinite.cofinite_inf_principal_neBot {α : Type u_2} {s : Set α} :
s.Infinite(Filter.cofinite ).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_nmem {α : Type u_2} {s : Set α} (hs : s.Finite) :
∀ᶠ (x : α) in Filter.cofinite, xs
theorem Finset.eventually_cofinite_nmem {α : Type u_2} (s : ) :
∀ᶠ (x : α) in Filter.cofinite, xs
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 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.cofinite.coprod 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
theorem Filter.disjoint_cofinite_left {α : Type u_2} {l : } :
Disjoint Filter.cofinite l sl, s.Finite
theorem Filter.disjoint_cofinite_right {α : Type u_2} {l : } :
Disjoint l Filter.cofinite sl, s.Finite
theorem Filter.countable_compl_ker {α : Type u_2} {l : } [l.IsCountablyGenerated] (h : Filter.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 : } [l.IsCountablyGenerated] (h : Filter.Tendsto f Filter.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 Set.Finite.cofinite_inf_principal_compl {α : Type u_2} {s : Set α} (hs : s.Finite) :
Filter.cofinite = Filter.cofinite
theorem Set.Finite.cofinite_inf_principal_diff {α : Type u_2} {s : Set α} {t : Set α} (ht : t.Finite) :
Filter.cofinite Filter.principal (s \ t) = Filter.cofinite
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) {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} [] {s : Set α} (hs : s.Nonempty) {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) :
a₀s, as, f 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 : s.Nonempty) {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
a₀s, as, f 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.