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
Instances for filter.cofinite
@[simp]
theorem filter.mem_cofinite {α : Type u_2} {s : set α} :
@[simp]
theorem filter.eventually_cofinite {α : Type u_2} {p : α Prop} :
(∀ᶠ (x : α) in filter.cofinite, p x) {x : α | ¬p x}.finite
@[protected, instance]
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) :
theorem set.finite.eventually_cofinite_nmem {α : Type u_2} {s : set α} (hs : s.finite) :
theorem finset.eventually_cofinite_nmem {α : Type u_2} (s : finset α) :
theorem filter.eventually_cofinite_ne {α : Type u_2} (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

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

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

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₀

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

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.

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