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

instance Filter.cofinite_neBot {α : Type u_1} [inst : Infinite α] :

Filter.NeBot Filter.cofinite

Equations

@Filter.cofinite_neBot = @Filter.cofinite_neBot.proof_1

@[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 ∈ s → f 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 ∈ s → f 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.