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.

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} [Infinite α] :
    Filter.cofinite.NeBot
    Equations
    • =
    @[simp]
    theorem Filter.cofinite_eq_bot_iff {α : Type u_2} :
    Filter.cofinite = Finite α
    @[simp]
    theorem Filter.cofinite_eq_bot {α : Type u_2} [Finite α] :
    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 Filter.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_nmem {α : Type u_2} {s : Set α} (hs : s.Finite) :
    ∀ᶠ (x : α) in Filter.cofinite, xs
    theorem Finset.eventually_cofinite_nmem {α : Type u_2} (s : Finset α) :
    ∀ᶠ (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 : Filter α} :
    l Filter.cofinite ∀ (x : α), {x} l
    theorem Filter.le_cofinite_iff_eventually_ne {α : Type u_2} {l : Filter α} :
    l Filter.cofinite ∀ (x : α), ∀ᶠ (y : α) in l, y x
    theorem Filter.atTop_le_cofinite {α : Type u_2} [Preorder α] [NoMaxOrder α] :
    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} [Finite ι] :
    (Filter.coprodᵢ fun (i : ι) => Filter.cofinite) = Filter.cofinite
    theorem Filter.disjoint_cofinite_left {α : Type u_2} {l : Filter α} :
    Disjoint Filter.cofinite l sl, s.Finite
    theorem Filter.disjoint_cofinite_right {α : Type u_2} {l : Filter α} :
    Disjoint l Filter.cofinite sl, s.Finite
    theorem Filter.countable_compl_ker {α : Type u_2} {l : Filter α} [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 : Filter β} [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.principal s = 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 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 : 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} [Nonempty α] [LinearOrder β] {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} [LinearOrder β] {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} [Nonempty α] [LinearOrder β] {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 : Function.Surjective f) :
    Filter.cofinite Filter.map f Filter.cofinite
    theorem Function.Injective.tendsto_cofinite {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.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 Function.Injective.comap_cofinite_eq {α : Type u_2} {β : Type u_3} {f : αβ} (hf : Function.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 : Function.Injective f) :
    Filter.Tendsto f Filter.atTop Filter.atTop

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