mathlib3 documentation

order.filter.cofinite

The cofinite filter #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define

cofinite: the filter of sets with finite complement

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

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

filter.cofinite = {sets := {s : set α | sᶜ.finite}, univ_sets := _, sets_of_superset := _, inter_sets := _}

Instances for filter.cofinite

filter.cofinite_ne_bot

@[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.has_basis_cofinite {α : Type u_2} :

filter.cofinite.has_basis (λ (s : set α), s.finite) has_compl.compl

@[protected, instance]

def filter.cofinite_ne_bot {α : Type u_2} [infinite α] :

filter.cofinite.ne_bot

theorem filter.frequently_cofinite_iff_infinite {α : Type u_2} {p : α → Prop} :

(∃ᶠ (x : α) in filter.cofinite , p x) ↔ {x : α | p x}.infinite

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 , x ∉ s

theorem finset.eventually_cofinite_nmem {α : Type u_2} (s : finset α) :

∀ᶠ (x : α) in filter.cofinite , x ∉ s

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.at_top_le_cofinite {α : Type u_2} [preorder α] [no_max_order α] :

filter.at_top ≤ filter.cofinite

If α is a preorder with no maximal element, then at_top ≤ 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_2} [finite ι] :

filter.Coprod (λ (i : ι), filter.cofinite) = filter.cofinite

Finite product of finite sets is finite

@[simp]

theorem filter.disjoint_cofinite_left {α : Type u_2} {l : filter α} :

disjoint filter.cofinite l ↔ ∃ (s : set α) (H : s ∈ l), s.finite

@[simp]

theorem filter.disjoint_cofinite_right {α : Type u_2} {l : filter α} :

disjoint l filter.cofinite ↔ ∃ (s : set α) (H : s ∈ l), s.finite

theorem nat.cofinite_eq_at_top :

filter.cofinite = filter.at_top

For natural numbers the filters cofinite and at_top coincide.

theorem nat.frequently_at_top_iff_infinite {p : ℕ → Prop} :

(∃ᶠ (n : ℕ) in filter.at_top , p n) ↔ {n : ℕ | p n}.infinite

theorem filter.tendsto.exists_within_forall_le {α : Type u_1} {β : Type u_2} [linear_order β] {s : set α} (hs : s.nonempty) {f : α → β} (hf : filter.tendsto f filter.cofinite filter.at_top) :

∃ (a₀ : α) (H : a₀ ∈ s), ∀ (a : α), a ∈ s → f a₀ ≤ f a

theorem filter.tendsto.exists_forall_le {α : Type u_2} {β : Type u_3} [nonempty α] [linear_order β] {f : α → β} (hf : filter.tendsto f filter.cofinite filter.at_top) :

∃ (a₀ : α), ∀ (a : α), f a₀ ≤ f a

theorem filter.tendsto.exists_within_forall_ge {α : Type u_2} {β : Type u_3} [linear_order β] {s : set α} (hs : s.nonempty) {f : α → β} (hf : filter.tendsto f filter.cofinite filter.at_bot) :

∃ (a₀ : α) (H : a₀ ∈ s), ∀ (a : α), a ∈ s → f a ≤ f a₀

theorem filter.tendsto.exists_forall_ge {α : Type u_2} {β : Type u_3} [nonempty α] [linear_order β] {f : α → β} (hf : filter.tendsto f filter.cofinite filter.at_bot) :

∃ (a₀ : α), ∀ (a : α), f a ≤ f a₀

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_at_top {f : ℕ → ℕ} (hf : function.injective f) :

filter.tendsto f filter.at_top filter.at_top

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