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

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Filter.mem_cofinite {α : Type u_1} {s : Set α} :
s Filter.cofinite Set.Finite (s)
@[simp]
theorem Filter.eventually_cofinite {α : Type u_1} {p : αProp} :
Filter.Eventually (fun x => p x) Filter.cofinite Set.Finite { x | ¬p x }
theorem Filter.hasBasis_cofinite {α : Type u_1} :
Filter.HasBasis Filter.cofinite (fun s => Set.Finite s) compl
@[simp]
theorem Filter.cofinite_eq_bot_iff {α : Type u_1} :
Filter.cofinite = Finite α
@[simp]
theorem Filter.cofinite_eq_bot {α : Type u_1} [inst : Finite α] :
Filter.cofinite =
theorem Filter.frequently_cofinite_iff_infinite {α : Type u_1} {p : αProp} :
Filter.Frequently (fun x => p x) Filter.cofinite Set.Infinite { x | p x }
theorem Set.Finite.compl_mem_cofinite {α : Type u_1} {s : Set α} (hs : Set.Finite s) :
s Filter.cofinite
theorem Set.Finite.eventually_cofinite_nmem {α : Type u_1} {s : Set α} (hs : Set.Finite s) :
Filter.Eventually (fun x => ¬x s) Filter.cofinite
theorem Finset.eventually_cofinite_nmem {α : Type u_1} (s : Finset α) :
Filter.Eventually (fun x => ¬x s) Filter.cofinite
theorem Set.infinite_iff_frequently_cofinite {α : Type u_1} {s : Set α} :
Set.Infinite s Filter.Frequently (fun x => x s) Filter.cofinite
theorem Filter.eventually_cofinite_ne {α : Type u_1} (x : α) :
Filter.Eventually (fun a => a x) Filter.cofinite
theorem Filter.le_cofinite_iff_compl_singleton_mem {α : Type u_1} {l : Filter α} :
l Filter.cofinite ∀ (x : α), {x} l
theorem Filter.le_cofinite_iff_eventually_ne {α : Type u_1} {l : Filter α} :
l Filter.cofinite ∀ (x : α), Filter.Eventually (fun y => y x) l
theorem Filter.atTop_le_cofinite {α : Type u_1} [inst : Preorder α] [inst : NoMaxOrder α] :
Filter.atTop Filter.cofinite

If α is a preorder with no maximal element, then atTop ≤ cofinite.

theorem Filter.comap_cofinite_le {α : Type u_1} {β : Type u_2} (f : αβ) :
Filter.comap f Filter.cofinite Filter.cofinite
theorem Filter.coprod_cofinite {α : Type u_1} {β : Type u_2} :
Filter.coprod Filter.cofinite 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_2} {α : ιType u_1} [inst : Finite ι] :
(Filter.coprodᵢ fun i => Filter.cofinite) = Filter.cofinite
@[simp]
theorem Filter.disjoint_cofinite_left {α : Type u_1} {l : Filter α} :
Disjoint Filter.cofinite l s, s l Set.Finite s
@[simp]
theorem Filter.disjoint_cofinite_right {α : Type u_1} {l : Filter α} :
Disjoint l Filter.cofinite s, s l Set.Finite 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} :
Filter.Frequently (fun n => p n) Filter.atTop Set.Infinite { n | p n }
theorem Filter.Tendsto.exists_within_forall_le {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {s : Set α} (hs : Set.Nonempty s) {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) :
a₀, a₀ s ∀ (a : α), a sf a₀ f a
theorem Filter.Tendsto.exists_forall_le {α : Type u_1} {β : Type u_2} [inst : Nonempty α] [inst : 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_1} [inst : LinearOrder β] {s : Set α} (hs : Set.Nonempty s) {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
a₀, a₀ s ∀ (a : α), a sf a f a₀
theorem Filter.Tendsto.exists_forall_ge {α : Type u_1} {β : Type u_2} [inst : Nonempty α] [inst : LinearOrder β] {f : αβ} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
a₀, ∀ (a : α), f a f a₀
theorem Function.Surjective.le_map_cofinite {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Surjective f) :
Filter.cofinite Filter.map f Filter.cofinite
theorem Function.Injective.tendsto_cofinite {α : Type u_1} {β : Type u_2} {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_1} {β : Type u_2} {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.