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} : Filter α

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

@[simp]

theorem Filter.mem_cofinite {α : Type u_2} {s : Set α} : s ∈ Filter.cofinite ↔ Set.Finite sᶜ

@[simp]

theorem Filter.eventually_cofinite {α : Type u_2} {p : α → Prop} : (∀ᶠ (x : α) in Filter.cofinite, p x) ↔ Set.Finite {x | ¬p x}

theorem Filter.hasBasis_cofinite {α : Type u_2} : Filter.HasBasis Filter.cofinite (fun s => Set.Finite s) compl

instance Filter.cofinite_neBot {α : Type u_2} [Infinite α] : Filter.NeBot Filter.cofinite

@[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) ↔ Set.Infinite {x | p x}

theorem Set.Finite.compl_mem_cofinite {α : Type u_2} {s : Set α} (hs : Set.Finite s) : sᶜ ∈ Filter.cofinite

theorem Set.Finite.eventually_cofinite_nmem {α : Type u_2} {s : Set α} (hs : Set.Finite s) : ∀ᶠ (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 α} : Set.Infinite s ↔ ∃ᶠ (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.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_1} {α : ι → Type u_4} [Finite ι] : (Filter.coprodᵢ fun i => Filter.cofinite) = Filter.cofinite

@[simp]

theorem Filter.disjoint_cofinite_left {α : Type u_2} {l : Filter α} : Disjoint Filter.cofinite l ↔ ∃ s, s ∈ l ∧ Set.Finite s

@[simp]

theorem Filter.disjoint_cofinite_right {α : Type u_2} {l : Filter α} : Disjoint l Filter.cofinite ↔ ∃ s, s ∈ l ∧ Set.Finite s

theorem Filter.countable_compl_ker {α : Type u_2} {l : Filter α} [Filter.IsCountablyGenerated l] (h : Filter.cofinite ≤ l) : Set.Countable (Filter.ker l)ᶜ

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 β} [Filter.IsCountablyGenerated l] (h : Filter.Tendsto f Filter.cofinite l) : Set.Countable (f ⁻¹' Filter.ker l)ᶜ

If f tends to a countably generated filter l along Filter.cofinite, then for all but countably many elements, f x ∈ l.ker.

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) ↔ Set.Infinite {n | p n}

theorem Filter.Tendsto.exists_within_forall_le {α : Type u_4} {β : Type u_5} [LinearOrder β] {s : Set α} (hs : Set.Nonempty s) {f : α → β} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) : ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → 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 : Set.Nonempty s) {f : α → β} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) : ∃ a₀, a₀ ∈ s ∧ ∀ (a : α), a ∈ s → 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.