# mathlibdocumentation

order.filter.cofinite

# The cofinite filter #

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

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

Equations
@[simp]
theorem filter.mem_cofinite {α : Type u_1} {s : set α} :
@[simp]
theorem filter.eventually_cofinite {α : Type u_1} {p : α → Prop} :
(∀ᶠ (x : α) in filter.cofinite, p x) {x : α | ¬p x}.finite
@[instance]
def filter.cofinite_ne_bot {α : Type u_1} [infinite α] :
theorem filter.frequently_cofinite_iff_infinite {α : Type u_1} {p : α → Prop} :
(∃ᶠ (x : α) in filter.cofinite, p x) {x : α | p x}.infinite
theorem filter.coprod_cofinite {α : Type u_1} {β : Type u_2} :

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} [fintype δ] :

Finite product of finite sets is finite

theorem set.finite.compl_mem_cofinite {α : Type u_1} {s : set α} (hs : s.finite) :
theorem set.finite.eventually_cofinite_nmem {α : Type u_1} {s : set α} (hs : s.finite) :
∀ᶠ (x : α) in filter.cofinite, x s
theorem finset.eventually_cofinite_nmem {α : Type u_1} (s : finset α) :
∀ᶠ (x : α) in filter.cofinite, x s
theorem set.infinite_iff_frequently_cofinite {α : Type u_1} {s : set α} :
s.infinite ∃ᶠ (x : α) in filter.cofinite, x s
theorem filter.eventually_cofinite_ne {α : Type u_1} (x : α) :
∀ᶠ (a : α) in filter.cofinite, a x

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_forall_le {α : Type u_1} {β : Type u_2} [nonempty α] [linear_order β] {f : α → β}  :
∃ (a₀ : α), ∀ (a : α), f a₀ f a
theorem filter.tendsto.exists_forall_ge {α : Type u_1} {β : Type u_2} [nonempty α] [linear_order β] {f : α → β}  :
∃ (a₀ : α), ∀ (a : α), f a f a₀