Finiteness and `Filter.atTop` and `Filter.atBot` filters #

This file contains results on Filter.atTop and Filter.atBot that depend on the finiteness theory developed in Mathlib.

source

theorem Filter.eventually_forall_ge_atTop {α : Type u_3} [Preorder α] {p : α → Prop} :

(∀ᶠ (x : α) in atTop , ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in atTop , p x

source

theorem Filter.eventually_forall_le_atBot {α : Type u_3} [Preorder α] {p : α → Prop} :

(∀ᶠ (x : α) in atBot , ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in atBot , p x

source

theorem Filter.Tendsto.eventually_forall_ge_atTop {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Tendsto f l atTop) (h_evtl : ∀ᶠ (x : β) in atTop , p x) :

∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y

source

theorem Filter.Tendsto.eventually_forall_le_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {p : β → Prop} {f : α → β} (hf : Tendsto f l atBot) (h_evtl : ∀ᶠ (x : β) in atBot , p x) :

∀ᶠ (x : α) in l, ∀ y ≤ f x, p y

Sequences #

source

theorem Filter.high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) (N : ℕ) :

∃ n ≥ N, ∀ k < n, u k < u n

If u is a sequence which is unbounded above, then after any point, it reaches a value strictly greater than all previous values.

source

theorem Filter.low_scores {β : Type u_4} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Tendsto u atTop atBot) (N : ℕ) :

∃ n ≥ N, ∀ k < n, u n < u k

If u is a sequence which is unbounded below, then after any point, it reaches a value strictly smaller than all previous values.

source

theorem Filter.frequently_high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) :

∃ᶠ (n : ℕ) in atTop , ∀ k < n, u k < u n

If u is a sequence which is unbounded above, then it Frequently reaches a value strictly greater than all previous values.

source

theorem Filter.frequently_low_scores {β : Type u_4} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Tendsto u atTop atBot) :

∃ᶠ (n : ℕ) in atTop , ∀ k < n, u n < u k

If u is a sequence which is unbounded below, then it Frequently reaches a value strictly smaller than all previous values.

source

theorem Filter.strictMono_subseq_of_tendsto_atTop {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Tendsto u atTop atTop) :

∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

source

theorem Filter.strictMono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ (n : ℕ), n ≤ u n) :

∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

source

theorem Filter.Eventually.atTop_of_arithmetic {p : ℕ → Prop} {n : ℕ} (hn : n ≠ 0) (hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop , p (n * a + k)) :

∀ᶠ (a : ℕ) in atTop , p a

source

theorem Filter.HasAntitoneBasis.subbasis_with_rel {α : Type u_3} {f : Filter α} {s : ℕ → Set α} (hs : f.HasAntitoneBasis s) {r : ℕ → ℕ → Prop} (hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop , r m n) :

∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ f.HasAntitoneBasis (s ∘ φ)

Given an antitone basis s : ℕ → Set α of a filter, extract an antitone subbasis s ∘ φ, φ : ℕ → ℕ, such that m < n implies r (φ m) (φ n). This lemma can be used to extract an antitone basis with basis sets decreasing "sufficiently fast".

source

theorem Nat.eventually_pow_lt_factorial_sub (c d : ℕ) :