Mathlib.Order.Filter.Cofinite

Filter.cofinite definition

: Filter α

Full source

/-- The cofinite filter is the filter of subsets whose complements are finite. -/
def cofinite : Filter α :=
  comk Set.Finite finite_empty (fun _t ht _s hsub ↦ ht.subset hsub) fun _ h _ ↦ h.union

Cofinite filter

Informal description

The cofinite filter on a type $\alpha$ is the filter consisting of all subsets of $\alpha$ whose complements are finite. In other words, a set $s$ is in the cofinite filter if and only if its complement $s^c$ is finite.

Filter.mem_cofinite theorem

{s : Set α} : s ∈ @cofinite α ↔ sᶜ.Finite

Full source

@[simp]
theorem mem_cofinite {s : Set α} : s ∈ @cofinite αs ∈ @cofinite α ↔ sᶜ.Finite :=
  Iff.rfl

Membership in Cofinite Filter is Equivalent to Finite Complement

Informal description

A subset $s$ of a type $\alpha$ belongs to the cofinite filter if and only if its complement $s^c$ is finite.

Filter.eventually_cofinite theorem

{p : α → Prop} : (∀ᶠ x in cofinite, p x) ↔ {x | ¬p x}.Finite

Full source

@[simp]
theorem eventually_cofinite {p : α → Prop} : (∀ᶠ x in cofinite, p x) ↔ { x | ¬p x }.Finite :=
  Iff.rfl

Characterization of Eventually in Cofinite Filter

Informal description

For any predicate $p$ on a type $\alpha$, the statement "eventually $p(x)$ holds in the cofinite filter" is equivalent to the condition that the set $\{x \mid \neg p(x)\}$ is finite.

Filter.hasBasis_cofinite theorem

: HasBasis cofinite (fun s : Set α => s.Finite) compl

Full source

theorem hasBasis_cofinite : HasBasis cofinite (fun s : Set α => s.Finite) compl :=
  ⟨fun s =>
    ⟨fun h => ⟨sᶜ, h, (compl_compl s).subset⟩, fun ⟨_t, htf, hts⟩ =>
      htf.subset <| compl_subset_comm.2 hts⟩⟩

Basis Characterization of the Cofinite Filter

Informal description

The cofinite filter on a type $\alpha$ has a basis consisting of the complements of finite subsets of $\alpha$. That is, a set $s$ is in the cofinite filter if and only if there exists a finite set $t \subseteq \alpha$ such that $s = t^c$.

Filter.cofinite_neBot instance

[Infinite α] : NeBot (@cofinite α)

Full source

instance cofinite_neBot [Infinite α] : NeBot (@cofinite α) :=
  hasBasis_cofinite.neBot_iff.2 fun hs => hs.infinite_compl.nonempty

Non-triviality of the Cofinite Filter on Infinite Types

Informal description

For any infinite type $\alpha$, the cofinite filter on $\alpha$ is non-trivial (i.e., it is not equal to the bottom filter).

Filter.cofinite_eq_bot_iff theorem

: @cofinite α = ⊥ ↔ Finite α

Full source

@[simp]
theorem cofinite_eq_bot_iff : @cofinite α = ⊥ ↔ Finite α := by
  simp [← empty_mem_iff_bot, finite_univ_iff]

Cofinite Filter Triviality Criterion: $\text{cofinite} = \bot \leftrightarrow \text{Finite } \alpha$

Informal description

The cofinite filter on a type $\alpha$ is equal to the bottom filter (the trivial filter) if and only if the type $\alpha$ is finite.

Filter.cofinite_eq_bot theorem

[Finite α] : @cofinite α = ⊥

Full source

@[simp]
theorem cofinite_eq_bot [Finite α] : @cofinite α = ⊥ := cofinite_eq_bot_iff.2 ‹_›

Cofinite Filter is Trivial on Finite Types

Informal description

For any finite type $\alpha$, the cofinite filter on $\alpha$ is equal to the trivial filter $\bot$.

Filter.frequently_cofinite_iff_infinite theorem

{p : α → Prop} : (∃ᶠ x in cofinite, p x) ↔ Set.Infinite {x | p x}

Full source

theorem frequently_cofinite_iff_infinite {p : α → Prop} :
    (∃ᶠ x in cofinite, p x) ↔ Set.Infinite { x | p x } := by
  simp only [Filter.Frequently, eventually_cofinite, not_not, Set.Infinite]

Frequently in Cofinite Filter iff Infinite Support

Informal description

For any predicate $p$ on a type $\alpha$, the statement that $p(x)$ holds frequently in the cofinite filter is equivalent to the set $\{x \mid p(x)\}$ being infinite.

Filter.frequently_cofinite_mem_iff_infinite theorem

{s : Set α} : (∃ᶠ x in cofinite, x ∈ s) ↔ s.Infinite

Full source

lemma frequently_cofinite_mem_iff_infinite {s : Set α} : (∃ᶠ x in cofinite, x ∈ s) ↔ s.Infinite :=
  frequently_cofinite_iff_infinite

Frequent Membership in Cofinite Filter iff Infinite Set

Informal description

For any set $s$ in a type $\alpha$, the statement that $x \in s$ holds frequently in the cofinite filter is equivalent to $s$ being infinite.

Filter.cofinite_inf_principal_neBot_iff theorem

{s : Set α} : (cofinite ⊓ 𝓟 s).NeBot ↔ s.Infinite

Full source

@[simp]
lemma cofinite_inf_principal_neBot_iff {s : Set α} : (cofinite ⊓ 𝓟 s).NeBot ↔ s.Infinite :=
  frequently_mem_iff_neBot.symm.trans frequently_cofinite_mem_iff_infinite

Non-triviality of Cofinite-Principal Filter Infimum iff Infinite Set

Informal description

For any set $s$ in a type $\alpha$, the filter obtained as the infimum of the cofinite filter and the principal filter generated by $s$ is non-trivial if and only if $s$ is infinite. In other words, $\text{cofinite} \sqcap \mathfrak{P}(s) \neq \bot$ if and only if $s$ is infinite.

Set.Finite.compl_mem_cofinite theorem

{s : Set α} (hs : s.Finite) : sᶜ ∈ @cofinite α

Full source

theorem _root_.Set.Finite.compl_mem_cofinite {s : Set α} (hs : s.Finite) : sᶜsᶜ ∈ @cofinite α :=
  mem_cofinite.2 <| (compl_compl s).symm ▸ hs

Complement of Finite Set Belongs to Cofinite Filter

Informal description

For any finite subset $s$ of a type $\alpha$, the complement of $s$ belongs to the cofinite filter on $\alpha$.

Set.Finite.eventually_cofinite_nmem theorem

{s : Set α} (hs : s.Finite) : ∀ᶠ x in cofinite, x ∉ s

Full source

theorem _root_.Set.Finite.eventually_cofinite_nmem {s : Set α} (hs : s.Finite) :
    ∀ᶠ x in cofinite, x ∉ s :=
  hs.compl_mem_cofinite

Eventual Non-Membership in Finite Sets via Cofinite Filter

Informal description

For any finite subset $s$ of a type $\alpha$, the event that an element $x$ does not belong to $s$ holds eventually in the cofinite filter on $\alpha$. In other words, $\{x \mid x \notin s\}$ is a member of the cofinite filter.

Finset.eventually_cofinite_nmem theorem

(s : Finset α) : ∀ᶠ x in cofinite, x ∉ s

Full source

theorem _root_.Finset.eventually_cofinite_nmem (s : Finset α) : ∀ᶠ x in cofinite, x ∉ s :=
  s.finite_toSet.eventually_cofinite_nmem

Eventual Non-Membership in Finite Sets via Cofinite Filter

Informal description

For any finite set $s$ (represented as a `Finset`) in a type $\alpha$, the event that an element $x$ does not belong to $s$ holds eventually in the cofinite filter on $\alpha$. In other words, $\{x \mid x \notin s\}$ is a member of the cofinite filter.

Set.infinite_iff_frequently_cofinite theorem

{s : Set α} : Set.Infinite s ↔ ∃ᶠ x in cofinite, x ∈ s

Full source

theorem _root_.Set.infinite_iff_frequently_cofinite {s : Set α} :
    Set.InfiniteSet.Infinite s ↔ ∃ᶠ x in cofinite, x ∈ s :=
  frequently_cofinite_iff_infinite.symm

Infinite Set Characterization via Cofinite Filter

Informal description

For any set $s$ in a type $\alpha$, the set $s$ is infinite if and only if the condition $x \in s$ holds frequently in the cofinite filter on $\alpha$.

Filter.eventually_cofinite_ne theorem

(x : α) : ∀ᶠ a in cofinite, a ≠ x

Full source

theorem eventually_cofinite_ne (x : α) : ∀ᶠ a in cofinite, a ≠ x :=
  (Set.finite_singleton x).eventually_cofinite_nmem

Eventual Non-Equality in Cofinite Filter

Informal description

For any element $x$ in a type $\alpha$, the event that an element $a$ is not equal to $x$ holds eventually in the cofinite filter on $\alpha$. In other words, $\{a \mid a \neq x\}$ is a member of the cofinite filter.

Filter.le_cofinite_iff_compl_singleton_mem theorem

: l ≤ cofinite ↔ ∀ x, { x }ᶜ ∈ l

Full source

theorem le_cofinite_iff_compl_singleton_mem : l ≤ cofinite ↔ ∀ x, {x}ᶜ ∈ l := by
  refine ⟨fun h x => h (finite_singleton x).compl_mem_cofinite, fun h s (hs : sᶜ.Finite) => ?_⟩
  rw [← compl_compl s, ← biUnion_of_singleton sᶜ, compl_iUnion₂, Filter.biInter_mem hs]
  exact fun x _ => h x

Characterization of Filters Contained in the Cofinite Filter via Singleton Complements

Informal description

A filter $l$ on a type $\alpha$ is contained in the cofinite filter if and only if for every element $x \in \alpha$, the complement of the singleton set $\{x\}$ belongs to $l$.

Filter.le_cofinite_iff_eventually_ne theorem

: l ≤ cofinite ↔ ∀ x, ∀ᶠ y in l, y ≠ x

Full source

theorem le_cofinite_iff_eventually_ne : l ≤ cofinite ↔ ∀ x, ∀ᶠ y in l, y ≠ x :=
  le_cofinite_iff_compl_singleton_mem

Characterization of Filters Contained in Cofinite via Eventual Non-Equality

Informal description

A filter $l$ on a type $\alpha$ is contained in the cofinite filter if and only if for every element $x \in \alpha$, the event that $y \neq x$ holds eventually in $l$.

Filter.atTop_le_cofinite theorem

[Preorder α] [NoTopOrder α] : (atTop : Filter α) ≤ cofinite

Full source

/-- If `α` is a preorder with no top element, then `atTop ≤ cofinite`. -/
theorem atTop_le_cofinite [Preorder α] [NoTopOrder α] : (atTop : Filter α) ≤ cofinite :=
  le_cofinite_iff_eventually_ne.mpr eventually_ne_atTop

Inclusion of `atTop` in the Cofinite Filter for Preorders without Top Elements

Informal description

For any preorder $\alpha$ with no top element, the filter `atTop` is contained in the cofinite filter. In other words, every set with finite complement in $\alpha$ contains all elements beyond some point in the order.

Filter.atBot_le_cofinite theorem

[Preorder α] [NoBotOrder α] : (atBot : Filter α) ≤ cofinite

Full source

/-- If `α` is a preorder with no bottom element, then `atBot ≤ cofinite`. -/
theorem atBot_le_cofinite [Preorder α] [NoBotOrder α] : (atBot : Filter α) ≤ cofinite :=
  le_cofinite_iff_eventually_ne.mpr eventually_ne_atBot

Inclusion of `atBot` in the Cofinite Filter for Preorders without Bottom Element

Informal description

For any preorder $\alpha$ with no bottom element, the filter `atBot` is contained in the cofinite filter. In other words, every set in the cofinite filter is eventually in the `atBot` filter.

Filter.comap_cofinite_le theorem

(f : α → β) : comap f cofinite ≤ cofinite

Full source

theorem comap_cofinite_le (f : α → β) : comap f cofinite ≤ cofinite :=
  le_cofinite_iff_eventually_ne.mpr fun x =>
    mem_comap.2 ⟨{f x}ᶜ, (finite_singleton _).compl_mem_cofinite, fun _ => ne_of_apply_ne f⟩

Pullback of Cofinite Filter is Contained in Cofinite Filter

Informal description

For any function $f : \alpha \to \beta$, the pullback of the cofinite filter on $\beta$ under $f$ is contained in the cofinite filter on $\alpha$. In other words, $\text{comap}_f(\text{cofinite}) \leq \text{cofinite}$.

Filter.coprod_cofinite theorem

: (cofinite : Filter α).coprod (cofinite : Filter β) = cofinite

Full source

/-- The coproduct of the cofinite filters on two types is the cofinite filter on their product. -/
theorem coprod_cofinite : (cofinite : Filter α).coprod (cofinite : Filter β) = cofinite :=
  Filter.coext fun s => by
    simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]

Coproduct of Cofinite Filters Equals Cofinite Filter on Product

Informal description

The coproduct of the cofinite filters on types $\alpha$ and $\beta$ is equal to the cofinite filter on their product type $\alpha \times \beta$. In other words, $(cofinite : \text{Filter } \alpha) \text{ coprod } (cofinite : \text{Filter } \beta) = cofinite$.

Filter.coprodᵢ_cofinite theorem

{α : ι → Type*} [Finite ι] : (Filter.coprodᵢ fun i => (cofinite : Filter (α i))) = cofinite

Full source

theorem coprodᵢ_cofinite {α : ι → Type*} [Finite ι] :
    (Filter.coprodᵢ fun i => (cofinite : Filter (α i))) = cofinite :=
  Filter.coext fun s => by
    simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]

Coproduct of Cofinite Filters Equals Cofinite Filter on Product Space

Informal description

For a finite index set $\iota$ and a family of types $\alpha_i$ indexed by $\iota$, the coproduct of the cofinite filters on each $\alpha_i$ is equal to the cofinite filter on the dependent product type $\prod_{i \in \iota} \alpha_i$. In other words, $\bigotimes_{i \in \iota} \text{cofinite} = \text{cofinite}$.

Filter.disjoint_cofinite_left theorem

: Disjoint cofinite l ↔ ∃ s ∈ l, Set.Finite s

Full source

theorem disjoint_cofinite_left : DisjointDisjoint cofinite l ↔ ∃ s ∈ l, Set.Finite s := by
  simp [l.basis_sets.disjoint_iff_right]

Disjointness of Cofinite Filter with Another Filter via Finite Sets

Informal description

The cofinite filter is disjoint from a filter $l$ if and only if there exists a finite set $s$ that belongs to $l$.

Filter.disjoint_cofinite_right theorem

: Disjoint l cofinite ↔ ∃ s ∈ l, Set.Finite s

Full source

theorem disjoint_cofinite_right : DisjointDisjoint l cofinite ↔ ∃ s ∈ l, Set.Finite s :=
  disjoint_comm.trans disjoint_cofinite_left

Disjointness of Filter with Cofinite Filter via Finite Sets

Informal description

A filter $l$ is disjoint from the cofinite filter if and only if there exists a finite set $s$ that belongs to $l$.

Filter.countable_compl_ker theorem

[l.IsCountablyGenerated] (h : cofinite ≤ l) : Set.Countable l.kerᶜ

Full source

/-- If `l ≥ Filter.cofinite` is a countably generated filter, then `l.ker` is cocountable. -/
theorem countable_compl_ker [l.IsCountablyGenerated] (h : cofinite ≤ l) : Set.Countable l.kerᶜ := by
  rcases exists_antitone_basis l with ⟨s, hs⟩
  simp only [hs.ker, iInter_true, compl_iInter]
  exact countable_iUnion fun n ↦ Set.Finite.countable <| h <| hs.mem _

Countability of Complement of Filter Kernel for Cofinite-Containing Filters

Informal description

Let $l$ be a countably generated filter on a type $\alpha$ such that the cofinite filter is contained in $l$ (i.e., $l \geq \text{cofinite}$). Then the complement of the kernel of $l$ is countable. Here, the kernel of $l$ is the intersection of all sets in $l$.

Filter.Tendsto.countable_compl_preimage_ker theorem

{f : α → β} {l : Filter β} [l.IsCountablyGenerated] (h : Tendsto f cofinite l) : Set.Countable (f ⁻¹' l.ker)ᶜ

Full source

/-- If `f` tends to a countably generated filter `l` along `Filter.cofinite`,
then for all but countably many elements, `f x ∈ l.ker`. -/
theorem Tendsto.countable_compl_preimage_ker {f : α → β}
    {l : Filter β} [l.IsCountablyGenerated] (h : Tendsto f cofinite l) :
    Set.Countable (f ⁻¹' l.ker)ᶜ := by rw [← ker_comap]; exact countable_compl_ker h.le_comap

Countability of Complement of Preimage Kernel for Cofinite-Convergent Functions

Informal description

Let $f : \alpha \to \beta$ be a function and $l$ a countably generated filter on $\beta$. If $f$ tends to $l$ along the cofinite filter, then the complement of the preimage of $l$'s kernel under $f$ is countable. Here, the kernel of $l$ is the intersection of all sets in $l$.

Filter.univ_pi_mem_pi theorem

 {α : ι → Type*} {s : ∀ i, Set (α i)} {l : ∀ i, Filter (α i)} (h : ∀ i, s i ∈ l i)
  (hfin : ∀ᶠ i in cofinite, s i = univ) : univ.pi s ∈ pi l

Full source

/-- Given a collection of filters `l i : Filter (α i)` and sets `s i ∈ l i`,
if all but finitely many of `s i` are the whole space,
then their indexed product `Set.pi Set.univ s` belongs to the filter `Filter.pi l`. -/
theorem univ_pi_mem_pi {α : ι → Type*} {s : ∀ i, Set (α i)} {l : ∀ i, Filter (α i)}
    (h : ∀ i, s i ∈ l i) (hfin : ∀ᶠ i in cofinite, s i = univ) : univuniv.pi s ∈ pi l := by
  filter_upwards [pi_mem_pi hfin fun i _ ↦ h i] with a ha i _
  if hi : s i = univ then
    simp [hi]
  else
    exact ha i hi

Product of Sets Belongs to Product Filter When Almost All Sets are Full

Informal description

Let $\{ \alpha_i \}_{i \in \iota}$ be a family of types, $\{ s_i \}_{i \in \iota}$ be a family of sets with $s_i \subseteq \alpha_i$ for each $i \in \iota$, and $\{ l_i \}_{i \in \iota}$ be a family of filters on $\alpha_i$. If $s_i \in l_i$ for every $i \in \iota$ and $s_i = \text{univ}$ for all but finitely many $i \in \iota$, then the product set $\prod_{i \in \iota} s_i$ belongs to the product filter $\prod_{i \in \iota} l_i$.

Filter.map_piMap_pi theorem

 {α β : ι → Type*} {f : ∀ i, α i → β i} (hf : ∀ᶠ i in cofinite, Surjective (f i)) (l : ∀ i, Filter (α i)) :
  map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i)

Full source

/-- Given a family of maps `f i : α i → β i` and a family of filters `l i : Filter (α i)`,
if all but finitely many of `f i` are surjective,
then the indexed product of `f i`s maps the indexed product of the filters `l i`
to the indexed products of their pushforwards under individual `f i`s.

See also `map_piMap_pi_finite` for the case of a finite index type.
-/
theorem map_piMap_pi {α β : ι → Type*} {f : ∀ i, α i → β i}
    (hf : ∀ᶠ i in cofinite, Surjective (f i)) (l : ∀ i, Filter (α i)) :
    map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) := by
  refine le_antisymm (tendsto_piMap_pi fun _ ↦ tendsto_map) ?_
  refine ((hasBasis_pi fun i ↦ (l i).basis_sets).map _).ge_iff.2 ?_
  rintro ⟨I, s⟩ ⟨hI : I.Finite, hs : ∀ i ∈ I, s i ∈ l i⟩
  classical
  rw [← univ_pi_piecewise_univ, piMap_image_univ_pi]
  refine univ_pi_mem_pi (fun i ↦ ?_) ?_
  · by_cases hi : i ∈ I
    · simpa [hi] using image_mem_map (hs i hi)
    · simp [hi]
  · filter_upwards [hf, hI.compl_mem_cofinite] with i hsurj (hiI : i ∉ I)
    simp [hiI, hsurj.range_eq]

Pushforward of Product Filter under Product Map with Cofinite Surjectivity

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ and $\{\beta_i\}_{i \in \iota}$ be families of types, and for each $i \in \iota$, let $f_i : \alpha_i \to \beta_i$ be a function. Suppose that for all but finitely many indices $i \in \iota$, the functions $f_i$ are surjective. Then, for any family of filters $\{l_i\}_{i \in \iota}$ where each $l_i$ is a filter on $\alpha_i$, the pushforward of the product filter $\prod_{i \in \iota} l_i$ under the product map $\prod_{i \in \iota} f_i$ is equal to the product filter $\prod_{i \in \iota} (f_i)_* l_i$, where $(f_i)_* l_i$ denotes the pushforward of $l_i$ under $f_i$.

Filter.map_piMap_pi_finite theorem

 {α β : ι → Type*} [Finite ι] (f : ∀ i, α i → β i) (l : ∀ i, Filter (α i)) :
  map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i)

Full source

/-- Given finite families of maps `f i : α i → β i` and of filters `l i : Filter (α i)`,
the indexed product of `f i`s maps the indexed product of the filters `l i`
to the indexed products of their pushforwards under individual `f i`s.

See also `map_piMap_pi` for a more general case.
-/
theorem map_piMap_pi_finite {α β : ι → Type*} [Finite ι]
    (f : ∀ i, α i → β i) (l : ∀ i, Filter (α i)) :
    map (Pi.map f) (pi l) = pi fun i ↦ map (f i) (l i) :=
  map_piMap_pi (by simp) l

Pushforward of Finite Product Filter under Product Map

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ and $\{\beta_i\}_{i \in \iota}$ be families of types indexed by a finite set $\iota$, and for each $i \in \iota$, let $f_i : \alpha_i \to \beta_i$ be a function. For any family of filters $\{l_i\}_{i \in \iota}$ where each $l_i$ is a filter on $\alpha_i$, the pushforward of the product filter $\prod_{i \in \iota} l_i$ under the product map $\prod_{i \in \iota} f_i$ is equal to the product filter $\prod_{i \in \iota} (f_i)_* l_i$, where $(f_i)_* l_i$ denotes the pushforward of $l_i$ under $f_i$.

Set.Finite.cofinite_inf_principal_compl theorem

{s : Set α} (hs : s.Finite) : cofinite ⊓ 𝓟 sᶜ = cofinite

Full source

lemma Set.Finite.cofinite_inf_principal_compl {s : Set α} (hs : s.Finite) :
    cofinitecofinite ⊓ 𝓟 sᶜ = cofinite := by
  simpa using hs.compl_mem_cofinite

Intersection of Cofinite Filter with Principal Complement Filter for Finite Sets

Informal description

For any finite subset $s$ of a type $\alpha$, the intersection of the cofinite filter on $\alpha$ with the principal filter generated by the complement of $s$ is equal to the cofinite filter itself, i.e., $\text{cofinite} \cap \mathcal{P}(s^c) = \text{cofinite}$.

Set.Finite.cofinite_inf_principal_diff theorem

{s t : Set α} (ht : t.Finite) : cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Full source

lemma Set.Finite.cofinite_inf_principal_diff {s t : Set α} (ht : t.Finite) :
    cofinitecofinite ⊓ 𝓟 (s \ t) = cofinitecofinite ⊓ 𝓟 s := by
  rw [diff_eq, ← inf_principal, ← inf_assoc, inf_right_comm, ht.cofinite_inf_principal_compl]

Cofinite Filter Stability under Set Difference with Finite Sets

Informal description

For any finite subset $t$ of a type $\alpha$ and any subset $s$ of $\alpha$, the intersection of the cofinite filter with the principal filter generated by the set difference $s \setminus t$ is equal to the intersection of the cofinite filter with the principal filter generated by $s$. That is, $\text{cofinite} \cap \mathcal{P}(s \setminus t) = \text{cofinite} \cap \mathcal{P}(s)$.

Nat.cofinite_eq_atTop theorem

: @cofinite ℕ = atTop

Full source

/-- For natural numbers the filters `Filter.cofinite` and `Filter.atTop` coincide. -/
theorem Nat.cofinite_eq_atTop : @cofinite ℕ = atTop := by
  refine le_antisymm ?_ atTop_le_cofinite
  refine atTop_basis.ge_iff.2 fun N _ => ?_
  simpa only [mem_cofinite, compl_Ici] using finite_lt_nat N

Equality of Cofinite and `atTop` Filters on Natural Numbers

Informal description

The cofinite filter on the natural numbers $\mathbb{N}$ coincides with the filter `atTop` (the filter of all subsets containing all sufficiently large natural numbers). In other words, a subset of $\mathbb{N}$ has finite complement if and only if it contains all natural numbers beyond some point.

Nat.frequently_atTop_iff_infinite theorem

{p : ℕ → Prop} : (∃ᶠ n in atTop, p n) ↔ Set.Infinite {n | p n}

Full source

theorem Nat.frequently_atTop_iff_infinite {p : ℕ → Prop} :
    (∃ᶠ n in atTop, p n) ↔ Set.Infinite { n | p n } := by
  rw [← Nat.cofinite_eq_atTop, frequently_cofinite_iff_infinite]

Frequently in `atTop` Filter on $\mathbb{N}$ iff Infinite Support

Informal description

For any predicate $p$ on the natural numbers $\mathbb{N}$, the statement that $p(n)$ holds frequently in the `atTop` filter is equivalent to the set $\{n \mid p(n)\}$ being infinite.

Nat.eventually_pos theorem

: ∀ᶠ (k : ℕ) in Filter.atTop, 0 < k

Full source

lemma Nat.eventually_pos : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < k :=
  Filter.eventually_of_mem (Filter.mem_atTop_sets.mpr ⟨1, fun _ hx ↦ hx⟩) (fun _ hx ↦ hx)

Positivity Eventually Holds for All Sufficiently Large Natural Numbers

Informal description

For the cofinite filter on the natural numbers, eventually every natural number $k$ is positive, i.e., $0 < k$ holds for all sufficiently large $k$.

Filter.Tendsto.exists_within_forall_le theorem

 {α β : Type*} [LinearOrder β] {s : Set α} (hs : s.Nonempty) {f : α → β}
  (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) : ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a

Full source

theorem Filter.Tendsto.exists_within_forall_le {α β : Type*} [LinearOrder β] {s : Set α}
    (hs : s.Nonempty) {f : α → β} (hf : Filter.Tendsto f Filter.cofinite Filter.atTop) :
    ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a := by
  rcases em (∃ y ∈ s, ∃ x, f y < x) with (⟨y, hys, x, hx⟩ | not_all_top)
  · -- the set of points `{y | f y < x}` is nonempty and finite, so we take `min` over this set
    have : { y | ¬x ≤ f y }.Finite := Filter.eventually_cofinite.mp (tendsto_atTop.1 hf x)
    simp only [not_le] at this
    obtain ⟨a₀, ⟨ha₀ : f a₀ < x, ha₀s⟩, others_bigger⟩ :=
      exists_min_image _ f (this.inter_of_left s) ⟨y, hx, hys⟩
    refine ⟨a₀, ha₀s, fun a has => (lt_or_le (f a) x).elim ?_ (le_trans ha₀.le)⟩
    exact fun h => others_bigger a ⟨h, has⟩
  · -- in this case, f is constant because all values are at top
    push_neg at not_all_top
    obtain ⟨a₀, ha₀s⟩ := hs
    exact ⟨a₀, ha₀s, fun a ha => not_all_top a ha (f a₀)⟩

Existence of Minimum Value for Functions Tending to Infinity on Nonempty Sets

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ linearly ordered, and let $s$ be a nonempty subset of $\alpha$. Given a function $f : \alpha \to \beta$ that tends to infinity in the cofinite filter (i.e., for any $M \in \beta$, the set $\{x \in \alpha \mid f(x) \leq M\}$ is finite), there exists an element $a_0 \in s$ such that $f(a_0) \leq f(a)$ for all $a \in s$.

Filter.Tendsto.exists_forall_le theorem

[Nonempty α] [LinearOrder β] {f : α → β} (hf : Tendsto f cofinite atTop) : ∃ a₀, ∀ a, f a₀ ≤ f a

Full source

theorem Filter.Tendsto.exists_forall_le [Nonempty α] [LinearOrder β] {f : α → β}
    (hf : Tendsto f cofinite atTop) : ∃ a₀, ∀ a, f a₀ ≤ f a :=
  let ⟨a₀, _, ha₀⟩ := hf.exists_within_forall_le univ_nonempty
  ⟨a₀, fun a => ha₀ a (mem_univ _)⟩

Existence of Global Minimum for Functions Tending to Infinity on Nonempty Domains

Informal description

Let $\alpha$ be a nonempty type and $\beta$ be a linearly ordered type. Given a function $f : \alpha \to \beta$ that tends to infinity in the cofinite filter (i.e., for any $M \in \beta$, the set $\{x \in \alpha \mid f(x) \leq M\}$ is finite), there exists an element $a_0 \in \alpha$ such that $f(a_0) \leq f(a)$ for all $a \in \alpha$.

Filter.Tendsto.exists_within_forall_ge theorem

 [LinearOrder β] {s : Set α} (hs : s.Nonempty) {f : α → β} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
  ∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀

Full source

theorem Filter.Tendsto.exists_within_forall_ge [LinearOrder β] {s : Set α} (hs : s.Nonempty)
    {f : α → β} (hf : Filter.Tendsto f Filter.cofinite Filter.atBot) :
    ∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀ :=
  @Filter.Tendsto.exists_within_forall_le _ βᵒᵈ _ _ hs _ hf

Existence of Maximum Value for Functions Tending to Negative Infinity on Nonempty Sets

Informal description

Let $\alpha$ be a type and $\beta$ be a linearly ordered type. Given a nonempty subset $s \subseteq \alpha$ and a function $f : \alpha \to \beta$ that tends to negative infinity in the cofinite filter (i.e., for any $M \in \beta$, the set $\{x \in \alpha \mid f(x) \geq M\}$ is finite), there exists an element $a_0 \in s$ such that $f(a) \leq f(a_0)$ for all $a \in s$.

Filter.Tendsto.exists_forall_ge theorem

[Nonempty α] [LinearOrder β] {f : α → β} (hf : Tendsto f cofinite atBot) : ∃ a₀, ∀ a, f a ≤ f a₀

Full source

theorem Filter.Tendsto.exists_forall_ge [Nonempty α] [LinearOrder β] {f : α → β}
    (hf : Tendsto f cofinite atBot) : ∃ a₀, ∀ a, f a ≤ f a₀ :=
  @Filter.Tendsto.exists_forall_le _ βᵒᵈ _ _ _ hf

Existence of Global Maximum for Functions Tending to Negative Infinity on Nonempty Domains

Informal description

Let $\alpha$ be a nonempty type and $\beta$ be a linearly ordered type. Given a function $f \colon \alpha \to \beta$ that tends to negative infinity in the cofinite filter (i.e., for any $M \in \beta$, the set $\{x \in \alpha \mid f(x) \geq M\}$ is finite), there exists an element $a_0 \in \alpha$ such that $f(a) \leq f(a_0)$ for all $a \in \alpha$.

Function.Surjective.le_map_cofinite theorem

{f : α → β} (hf : Surjective f) : cofinite ≤ map f cofinite

Full source

theorem Function.Surjective.le_map_cofinite {f : α → β} (hf : Surjective f) :
    cofinite ≤ map f cofinite := fun _ h => .of_preimage h hf

Surjective Functions Preserve Cofinite Filter Containment

Informal description

For any surjective function $f : \alpha \to \beta$, the cofinite filter on $\alpha$ is contained in the pushforward of the cofinite filter on $\beta$ under $f$. In other words, if $f$ is surjective, then for any set $s \subseteq \alpha$ with finite complement, the image $f(s)$ has finite complement in $\beta$.

Function.Injective.tendsto_cofinite theorem

{f : α → β} (hf : Injective f) : Tendsto f cofinite cofinite

Full source

/-- 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.tendsto_cofinite {f : α → β} (hf : Injective f) :
    Tendsto f cofinite cofinite := fun _ h => h.preimage hf.injOn

Injective Functions Preserve Cofinite Filters

Informal description

For any injective function $f \colon \alpha \to \beta$, the pushforward of the cofinite filter on $\alpha$ under $f$ is contained in the cofinite filter on $\beta$. In other words, if $f$ is injective, then the image of any cofinite set in $\alpha$ is cofinite in $\beta$.

Filter.Tendsto.cofinite_of_finite_preimage_singleton theorem

{f : α → β} (hf : ∀ b, Finite (f ⁻¹' { b })) : Tendsto f cofinite cofinite

Full source

/-- For a function with finite fibres, inverse images of finite sets are finite. -/
theorem Filter.Tendsto.cofinite_of_finite_preimage_singleton {f : α → β}
    (hf : ∀ b, Finite (f ⁻¹' {b})) : Tendsto f cofinite cofinite :=
  fun _ h => h.preimage' fun b _ ↦ hf b

Function with finite fibers preserves cofinite filter

Informal description

For a function $f: \alpha \to \beta$ such that the preimage $f^{-1}(\{b\})$ is finite for every $b \in \beta$, the function $f$ tends to the cofinite filter on $\beta$ along the cofinite filter on $\alpha$. In other words, if $S \subseteq \beta$ has finite complement, then $f^{-1}(S) \subseteq \alpha$ also has finite complement.

Function.Injective.comap_cofinite_eq theorem

{f : α → β} (hf : Injective f) : comap f cofinite = cofinite

Full source

/-- 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.comap_cofinite_eq {f : α → β} (hf : Injective f) :
    comap f cofinite = cofinite :=
  (comap_cofinite_le f).antisymm hf.tendsto_cofinite.le_comap

Equality of Cofinite Filters under Injective Pullback

Informal description

For any injective function $f \colon \alpha \to \beta$, the pullback of the cofinite filter on $\beta$ under $f$ is equal to the cofinite filter on $\alpha$. In other words, $\text{comap}_f(\text{cofinite}) = \text{cofinite}$.

Function.Injective.nat_tendsto_atTop theorem

{f : ℕ → ℕ} (hf : Injective f) : Tendsto f atTop atTop

Full source

/-- An injective sequence `f : ℕ → ℕ` tends to infinity at infinity. -/
theorem Function.Injective.nat_tendsto_atTop {f : ℕ → ℕ} (hf : Injective f) :
    Tendsto f atTop atTop :=
  Nat.cofinite_eq_atTop ▸ hf.tendsto_cofinite

Injective sequences of natural numbers tend to infinity

Informal description

For any injective function $f \colon \mathbb{N} \to \mathbb{N}$, the sequence $f(n)$ tends to infinity as $n$ tends to infinity. In other words, for any $N \in \mathbb{N}$, there exists $M \in \mathbb{N}$ such that for all $n \geq M$, we have $f(n) \geq N$.

TODO