Module docstring
{"# Basic results on Filter.atTop and Filter.atBot filters
In this file we prove many lemmas like “if f → +∞, then f ± c → +∞”.
","### Sequences
"}
Filter.hasAntitoneBasis_atTop
theorem
[Nonempty α] : (@atTop α _).HasAntitoneBasis Ici
Full source
theorem hasAntitoneBasis_atTop [Nonempty α] : (@atTop α _).HasAntitoneBasis Ici :=
.iInf_principal fun _ _ ↦ Ici_subset_Ici.2Informal description
For any nonempty preorder $\alpha$, the filter `atTop` has an antitone basis consisting of the left-closed right-infinite intervals $[a, \infty)$ for $a \in \alpha$. In other words, the family of sets $\{[a, \infty) \mid a \in \alpha\}$ forms a decreasing basis for the filter `atTop`.
Filter.atTop_basis
theorem
[Nonempty α] : (@atTop α _).HasBasis (fun _ => True) Ici
Full source
theorem atTop_basis [Nonempty α] : (@atTop α _).HasBasis (fun _ => True) Ici :=
hasAntitoneBasis_atTop.1Informal description
For any nonempty preorder $\alpha$, the filter `atTop` has a basis consisting of all left-closed right-infinite intervals $[a, \infty)$ for $a \in \alpha$. That is, a set belongs to `atTop` if and only if it contains some interval $[a, \infty)$.
Filter.atTop_basis_Ioi
theorem
[Nonempty α] [NoMaxOrder α] : (@atTop α _).HasBasis (fun _ => True) Ioi
Full source
lemma atTop_basis_Ioi [Nonempty α] [NoMaxOrder α] : (@atTop α _).HasBasis (fun _ => True) Ioi :=
atTop_basis.to_hasBasis (fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩) fun a ha =>
(exists_gt a).imp fun _b hb => ⟨ha, Ici_subset_Ioi.2 hb⟩Informal description
For any nonempty preorder $\alpha$ without maximal elements, the filter `atTop` has a basis consisting of all left-open right-infinite intervals $(a, \infty)$ for $a \in \alpha$. That is, a set belongs to `atTop` if and only if it contains some interval $(a, \infty)$.
Filter.atTop_basis_Ioi'
theorem
[NoMaxOrder α] (a : α) : atTop.HasBasis (a < ·) Ioi
Full source
lemma atTop_basis_Ioi' [NoMaxOrder α] (a : α) : atTop.HasBasis (a < ·) Ioi := by
have : Nonempty α := ⟨a⟩
refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
obtain ⟨d, hcd⟩ := exists_gt c
exact ⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩Informal description
For any preorder $\alpha$ without maximal elements and any element $a \in \alpha$, the filter `atTop` has a basis consisting of all left-open right-infinite intervals $(b, \infty)$ where $b > a$. That is, a set belongs to `atTop` if and only if it contains some interval $(b, \infty)$ with $b > a$.
Filter.atTop_basis'
theorem
(a : α) : atTop.HasBasis (a ≤ ·) Ici
Full source
theorem atTop_basis' (a : α) : atTop.HasBasis (a ≤ ·) Ici := by
have : Nonempty α := ⟨a⟩
refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩Informal description
For any element $a$ in a preorder $\alpha$, the filter `atTop` has a basis consisting of all left-closed right-infinite intervals $[b, \infty)$ where $b \geq a$. That is, a set belongs to `atTop` if and only if it contains some interval $[b, \infty)$ with $b \geq a$.
Filter.atTop_neBot
theorem
: NeBot (atTop : Filter α)
Full source
@[instance]
lemma atTop_neBot : NeBot (atTop : Filter α) := atTop_basis.neBot_iff.2 fun _ => nonempty_IciInformal description
The filter `atTop` on a preorder $\alpha$ is non-trivial (i.e., does not contain the empty set).
Filter.atTop_neBot_iff
theorem
{α : Type*} [Preorder α] : (atTop : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≤ ·)
Full source
theorem atTop_neBot_iff {α : Type*} [Preorder α] :
(atTop : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≤ ·) := by
refine ⟨fun h ↦ ⟨nonempty_of_neBot atTop, ⟨fun x y ↦ ?_⟩⟩, fun ⟨h₁, h₂⟩ ↦ atTop_neBot⟩
exact ((eventually_ge_atTop x).and (eventually_ge_atTop y)).existsInformal description
For a preorder $\alpha$, the filter `atTop` is non-trivial if and only if $\alpha$ is nonempty and directed with respect to the relation $\leq$.
Filter.atBot_neBot_iff
theorem
{α : Type*} [Preorder α] : (atBot : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≥ ·)
Full source
theorem atBot_neBot_iff {α : Type*} [Preorder α] :
(atBot : Filter α).NeBot ↔ Nonempty α ∧ IsDirected α (· ≥ ·) :=
atTop_neBot_iff (α := αᵒᵈ)Informal description
For a preorder $\alpha$, the filter `atBot` is non-trivial if and only if $\alpha$ is nonempty and directed with respect to the relation $\geq$.
Filter.mem_atTop_sets
theorem
{s : Set α} : s ∈ (atTop : Filter α) ↔ ∃ a : α, ∀ b ≥ a, b ∈ s
Full source
@[simp] lemma mem_atTop_sets {s : Set α} : s ∈ (atTop : Filter α)s ∈ (atTop : Filter α) ↔ ∃ a : α, ∀ b ≥ a, b ∈ s :=
atTop_basis.mem_iff.trans <| exists_congr fun _ => iff_of_eq (true_and _)Informal description
For any set $s$ in a preorder $\alpha$, $s$ belongs to the `atTop` filter if and only if there exists an element $a \in \alpha$ such that for all $b \geq a$, $b$ is in $s$.
Filter.eventually_atTop
theorem
: (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ b ≥ a, p b
Full source
@[simp] lemma eventually_atTop : (∀ᶠ x in atTop, p x) ↔ ∃ a, ∀ b ≥ a, p b := mem_atTop_setsInformal description
For any predicate $p$ on a preorder $\alpha$, the following are equivalent:
1. The predicate $p$ holds eventually in the `atTop` filter (i.e., $p(x)$ holds for all sufficiently large $x$).
2. There exists an element $a \in \alpha$ such that for all $b \geq a$, $p(b)$ holds.
Filter.frequently_atTop
theorem
: (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b ≥ a, p b
Full source
theorem frequently_atTop : (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b ≥ a, p b :=
atTop_basis.frequently_iff.trans <| by simpInformal description
For any predicate $p$ on a preorder $\alpha$, the following are equivalent:
1. The predicate $p$ holds frequently in the `atTop` filter (i.e., there exists infinitely many $x$ tending to infinity where $p(x)$ holds).
2. For every element $a \in \alpha$, there exists an element $b \geq a$ such that $p(b)$ holds.
In other words, $p$ holds frequently at infinity if and only if for any threshold $a$, there exists some $b$ beyond $a$ where $p(b)$ is true.
Filter.exists_eventually_atTop
theorem
{r : α → β → Prop} : (∃ b, ∀ᶠ a in atTop, r a b) ↔ ∀ᶠ a₀ in atTop, ∃ b, ∀ a ≥ a₀, r a b
Full source
lemma exists_eventually_atTop {r : α → β → Prop} :
(∃ b, ∀ᶠ a in atTop, r a b) ↔ ∀ᶠ a₀ in atTop, ∃ b, ∀ a ≥ a₀, r a b := by
simp_rw [eventually_atTop, ← exists_swap (α := α)]
exact exists_congr fun a ↦ .symm <| forall_ge_iff <| Monotone.exists fun _ _ _ hb H n hn ↦
H n (hb.trans hn)Informal description
For any relation $r : \alpha \to \beta \to \text{Prop}$, the following are equivalent:
1. There exists $b \in \beta$ such that for all sufficiently large $a \in \alpha$, $r(a, b)$ holds.
2. For all sufficiently large $a_0 \in \alpha$, there exists $b \in \beta$ such that for all $a \geq a_0$, $r(a, b)$ holds.
In other words, the existence of a uniform witness $b$ that works for all large enough $a$ is equivalent to the statement that for all large enough starting points $a_0$, there exists some witness $b$ that works for all $a \geq a_0$.
Filter.map_atTop_eq
theorem
{f : α → β} : atTop.map f = ⨅ a, 𝓟 (f '' {a' | a ≤ a'})
Full source
theorem map_atTop_eq {f : α → β} : atTop.map f = ⨅ a, 𝓟 (f '' { a' | a ≤ a' }) :=
(atTop_basis.map f).eq_iInfInformal description
For any function $f : \alpha \to \beta$ between preordered types, the image filter of the `atTop` filter under $f$ is equal to the infimum over all $a \in \alpha$ of the principal filter generated by the image of the set $\{a' \in \alpha \mid a \leq a'\}$ under $f$. That is,
\[ \text{map}\, f\, \text{atTop} = \bigsqcap_{a \in \alpha} \mathcal{P}(f([a, \infty))). \]
Filter.frequently_atTop'
theorem
[NoMaxOrder α] : (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b > a, p b
Full source
theorem frequently_atTop' [NoMaxOrder α] : (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b > a, p b :=
atTop_basis_Ioi.frequently_iff.trans <| by simpInformal description
For a preorder $\alpha$ with no maximal elements, a property $p$ holds frequently in the `atTop` filter if and only if for every element $a \in \alpha$, there exists an element $b > a$ such that $p(b)$ holds. In other words, $\exists^l x \text{ in } \text{atTop}, p(x) \leftrightarrow \forall a \in \alpha, \exists b > a, p(b)$.
Filter.atBot_basis_Iio
theorem
[Nonempty α] [NoMinOrder α] : (@atBot α _).HasBasis (fun _ => True) Iio
Full source
lemma atBot_basis_Iio [Nonempty α] [NoMinOrder α] : (@atBot α _).HasBasis (fun _ => True) Iio :=
atTop_basis_Ioi (α := αᵒᵈ)Informal description
For any nonempty preorder $\alpha$ without minimal elements, the filter `atBot` has a basis consisting of all left-infinite right-open intervals $(-\infty, a)$ for $a \in \alpha$. That is, a set belongs to `atBot` if and only if it contains some interval $(-\infty, a)$.
Filter.atBot_basis'
theorem
(a : α) : (@atBot α _).HasBasis (fun x => x ≤ a) Iic
Full source
lemma atBot_basis' (a : α) : (@atBot α _).HasBasis (fun x => x ≤ a) Iic := atTop_basis' (α := αᵒᵈ) _Informal description
For any element $a$ in a preorder $\alpha$, the filter `atBot` has a basis consisting of all left-infinite right-closed intervals $(-\infty, b]$ where $b \leq a$. That is, a set belongs to `atBot` if and only if it contains some interval $(-\infty, b]$ with $b \leq a$.
Filter.atBot_basis
theorem
: (@atBot α _).HasBasis (fun _ => True) Iic
Full source
lemma atBot_basis : (@atBot α _).HasBasis (fun _ => True) Iic := atTop_basis (α := αᵒᵈ)Informal description
The filter `atBot` on a preorder $\alpha$ has a basis consisting of all left-infinite right-closed intervals $(-\infty, b]$ for $b \in \alpha$. That is, a set belongs to `atBot` if and only if it contains some interval $(-\infty, b]$.
Filter.atBot_neBot
theorem
: NeBot (atBot : Filter α)
Full source
@[instance] lemma atBot_neBot : NeBot (atBot : Filter α) := atTop_neBot (α := αᵒᵈ)Informal description
The filter `atBot` on a preorder $\alpha$ is non-trivial, meaning it does not contain the empty set.
Filter.mem_atBot_sets
theorem
{s : Set α} : s ∈ (atBot : Filter α) ↔ ∃ a : α, ∀ b ≤ a, b ∈ s
Full source
@[simp] lemma mem_atBot_sets {s : Set α} : s ∈ (atBot : Filter α)s ∈ (atBot : Filter α) ↔ ∃ a : α, ∀ b ≤ a, b ∈ s :=
mem_atTop_sets (α := αᵒᵈ)Informal description
For any set $s$ in a preorder $\alpha$, $s$ belongs to the `atBot` filter if and only if there exists an element $a \in \alpha$ such that for all $b \leq a$, $b$ is in $s$.
Filter.eventually_atBot
theorem
: (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ b ≤ a, p b
Full source
@[simp] lemma eventually_atBot : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ b ≤ a, p b := mem_atBot_setsInformal description
For any predicate $p$ on a preorder $\alpha$, the following are equivalent:
1. The predicate $p$ holds eventually in the `atBot` filter (i.e., $p(x)$ holds for all sufficiently small $x$).
2. There exists an element $a \in \alpha$ such that for all $b \leq a$, $p(b)$ holds.
In other words, $p$ holds eventually at negative infinity if and only if there exists some threshold $a$ such that $p$ holds for all elements below $a$.
Filter.frequently_atBot
theorem
: (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b ≤ a, p b
Full source
theorem frequently_atBot : (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b ≤ a, p b := frequently_atTop (α := αᵒᵈ)Informal description
For any predicate $p$ on a preorder $\alpha$, the following are equivalent:
1. The predicate $p$ holds frequently in the `atBot` filter (i.e., there exist infinitely many $x$ tending to negative infinity where $p(x)$ holds).
2. For every element $a \in \alpha$, there exists an element $b \leq a$ such that $p(b)$ holds.
In other words, $p$ holds frequently at negative infinity if and only if for any threshold $a$, there exists some $b$ below $a$ where $p(b)$ is true.
Filter.exists_eventually_atBot
theorem
{r : α → β → Prop} : (∃ b, ∀ᶠ a in atBot, r a b) ↔ ∀ᶠ a₀ in atBot, ∃ b, ∀ a ≤ a₀, r a b
Full source
lemma exists_eventually_atBot {r : α → β → Prop} :
(∃ b, ∀ᶠ a in atBot, r a b) ↔ ∀ᶠ a₀ in atBot, ∃ b, ∀ a ≤ a₀, r a b :=
exists_eventually_atTop (α := αᵒᵈ)Informal description
For any relation $r : \alpha \to \beta \to \text{Prop}$, the following are equivalent:
1. There exists $b \in \beta$ such that for all sufficiently small $a \in \alpha$, $r(a, b)$ holds.
2. For all sufficiently small $a_0 \in \alpha$, there exists $b \in \beta$ such that for all $a \leq a_0$, $r(a, b)$ holds.
In other words, the existence of a uniform witness $b$ that works for all small enough $a$ is equivalent to the statement that for all small enough starting points $a_0$, there exists some witness $b$ that works for all $a \leq a_0$.
Filter.map_atBot_eq
theorem
{f : α → β} : atBot.map f = ⨅ a, 𝓟 (f '' {a' | a' ≤ a})
Full source
theorem map_atBot_eq {f : α → β} : atBot.map f = ⨅ a, 𝓟 (f '' { a' | a' ≤ a }) :=
map_atTop_eq (α := αᵒᵈ)Informal description
For any function $f : \alpha \to \beta$ between preordered types, the image filter of the `atBot` filter under $f$ is equal to the infimum over all $a \in \alpha$ of the principal filter generated by the image of the set $\{a' \in \alpha \mid a' \leq a\}$ under $f$. That is,
\[ \text{map}\, f\, \text{atBot} = \bigsqcap_{a \in \alpha} \mathcal{P}(f((-\infty, a])). \]
Filter.frequently_atBot'
theorem
[NoMinOrder α] : (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b < a, p b
Full source
theorem frequently_atBot' [NoMinOrder α] : (∃ᶠ x in atBot, p x) ↔ ∀ a, ∃ b < a, p b :=
frequently_atTop' (α := αᵒᵈ)Informal description
For a preorder $\alpha$ with no minimal elements, a property $p$ holds frequently in the `atBot` filter if and only if for every element $a \in \alpha$, there exists an element $b < a$ such that $p(b)$ holds.
Filter.extraction_of_frequently_atTop
theorem
{P : ℕ → Prop} (h : ∃ᶠ n in atTop, P n) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n)
Full source
theorem extraction_of_frequently_atTop {P : ℕ → Prop} (h : ∃ᶠ n in atTop, P n) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n) := by
rw [frequently_atTop'] at h
exact Nat.exists_strictMono_subsequence hInformal description
For any predicate $P$ on natural numbers that holds frequently in the `atTop` filter (i.e., for every $N \in \mathbb{N}$, there exists $n > N$ such that $P(n)$ holds), there exists a strictly increasing function $\varphi \colon \mathbb{N} \to \mathbb{N}$ such that $P(\varphi(n))$ holds for all $n \in \mathbb{N}$.
Filter.extraction_of_eventually_atTop
theorem
{P : ℕ → Prop} (h : ∀ᶠ n in atTop, P n) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n)
Full source
theorem extraction_of_eventually_atTop {P : ℕ → Prop} (h : ∀ᶠ n in atTop, P n) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n) :=
extraction_of_frequently_atTop h.frequentlyInformal description
For any predicate $P$ on natural numbers that holds eventually in the `atTop` filter (i.e., there exists $N \in \mathbb{N}$ such that $P(n)$ holds for all $n \geq N$), there exists a strictly increasing function $\varphi \colon \mathbb{N} \to \mathbb{N}$ such that $P(\varphi(n))$ holds for all $n \in \mathbb{N}$.
Filter.extraction_forall_of_frequently
theorem
{P : ℕ → ℕ → Prop} (h : ∀ n, ∃ᶠ k in atTop, P n k) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n)
Full source
theorem extraction_forall_of_frequently {P : ℕ → ℕ → Prop} (h : ∀ n, ∃ᶠ k in atTop, P n k) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) := by
simp only [frequently_atTop'] at h
choose u hu hu' using h
use (fun n => Nat.recOn n (u 0 0) fun n v => u (n + 1) v : ℕ → ℕ)
constructor
· apply strictMono_nat_of_lt_succ
intro n
apply hu
· intro n
cases n <;> simp [hu']Informal description
For any family of predicates $P : \mathbb{N} \times \mathbb{N} \to \text{Prop}$ such that for every $n \in \mathbb{N}$, the set $\{k \in \mathbb{N} \mid P(n, k)\}$ is frequently true in the filter `atTop`, there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that $P(n, \varphi(n))$ holds for all $n \in \mathbb{N}$.
Filter.extraction_forall_of_eventually
theorem
{P : ℕ → ℕ → Prop} (h : ∀ n, ∀ᶠ k in atTop, P n k) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n)
Full source
theorem extraction_forall_of_eventually {P : ℕ → ℕ → Prop} (h : ∀ n, ∀ᶠ k in atTop, P n k) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) :=
extraction_forall_of_frequently fun n => (h n).frequentlyInformal description
For any family of predicates $P : \mathbb{N} \times \mathbb{N} \to \text{Prop}$ such that for every $n \in \mathbb{N}$, the predicate $P(n, k)$ holds for all sufficiently large $k$ (i.e., $\forall n, \exists N, \forall k \geq N, P(n, k)$), there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that $P(n, \varphi(n))$ holds for all $n \in \mathbb{N}$.
Filter.extraction_forall_of_eventually'
theorem
{P : ℕ → ℕ → Prop} (h : ∀ n, ∃ N, ∀ k ≥ N, P n k) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n)
Full source
theorem extraction_forall_of_eventually' {P : ℕ → ℕ → Prop} (h : ∀ n, ∃ N, ∀ k ≥ N, P n k) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P n (φ n) :=
extraction_forall_of_eventually (by simp [eventually_atTop, h])Informal description
For any family of predicates $P : \mathbb{N} \times \mathbb{N} \to \text{Prop}$ such that for every $n \in \mathbb{N}$, there exists a natural number $N$ such that for all $k \geq N$, $P(n, k)$ holds, there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that $P(n, \varphi(n))$ holds for all $n \in \mathbb{N}$.
Filter.inf_map_atTop_neBot_iff
theorem
[Nonempty α] : NeBot (F ⊓ map u atTop) ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U
Informal description
For a nonempty type $\alpha$ and a filter $F$ on $\alpha$, the filter $F \sqcap \text{map } u \text{ atTop}$ is non-trivial if and only if for every set $U$ in $F$ and every natural number $N$, there exists an $n \geq N$ such that $u(n) \in U$.
Filter.exists_le_of_tendsto_atTop
theorem
(h : Tendsto u atTop atTop) (a : α) (b : β) : ∃ a' ≥ a, b ≤ u a'
Full source
lemma exists_le_of_tendsto_atTop (h : Tendsto u atTop atTop) (a : α) (b : β) :
∃ a' ≥ a, b ≤ u a' := by
have : Nonempty α := ⟨a⟩
have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x :=
(eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)
exact this.existsInformal description
Let $u : \alpha \to \beta$ be a function between preorders $\alpha$ and $\beta$. If $u$ tends to infinity (i.e., $\text{Tendsto } u \text{ atTop atTop}$), then for any elements $a \in \alpha$ and $b \in \beta$, there exists an element $a' \in \alpha$ such that $a' \geq a$ and $b \leq u(a')$.
Filter.exists_le_of_tendsto_atBot
theorem
(h : Tendsto u atTop atBot) : ∀ a b, ∃ a' ≥ a, u a' ≤ b
Full source
theorem exists_le_of_tendsto_atBot (h : Tendsto u atTop atBot) :
∀ a b, ∃ a' ≥ a, u a' ≤ b := exists_le_of_tendsto_atTop (β := βᵒᵈ) hInformal description
Let $u : \alpha \to \beta$ be a function between preorders $\alpha$ and $\beta$. If $u$ tends to negative infinity (i.e., $\text{Tendsto } u \text{ atTop atBot}$), then for any elements $a \in \alpha$ and $b \in \beta$, there exists an element $a' \in \alpha$ such that $a' \geq a$ and $u(a') \leq b$.
Filter.exists_lt_of_tendsto_atTop
theorem
[NoMaxOrder β] (h : Tendsto u atTop atTop) (a : α) (b : β) : ∃ a' ≥ a, b < u a'
Full source
theorem exists_lt_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto u atTop atTop) (a : α) (b : β) :
∃ a' ≥ a, b < u a' := by
obtain ⟨b', hb'⟩ := exists_gt b
rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩
exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩Informal description
Let $\alpha$ and $\beta$ be preorders, with $\beta$ having no maximal elements. If a function $u : \alpha \to \beta$ tends to infinity (i.e., $\lim_{x \to \infty} u(x) = \infty$), then for any $a \in \alpha$ and $b \in \beta$, there exists $a' \in \alpha$ with $a' \geq a$ such that $b < u(a')$.
Filter.exists_lt_of_tendsto_atBot
theorem
[NoMinOrder β] (h : Tendsto u atTop atBot) : ∀ a b, ∃ a' ≥ a, u a' < b
Full source
theorem exists_lt_of_tendsto_atBot [NoMinOrder β] (h : Tendsto u atTop atBot) :
∀ a b, ∃ a' ≥ a, u a' < b := exists_lt_of_tendsto_atTop (β := βᵒᵈ) hInformal description
Let $\alpha$ and $\beta$ be preorders, with $\beta$ having no minimal elements. If a function $u : \alpha \to \beta$ tends to negative infinity (i.e., $\lim_{x \to \infty} u(x) = -\infty$), then for any $a \in \alpha$ and $b \in \beta$, there exists $a' \in \alpha$ with $a' \geq a$ such that $u(a') < b$.
Filter.inf_map_atBot_neBot_iff
theorem
: NeBot (F ⊓ map u atBot) ↔ ∀ U ∈ F, ∀ N, ∃ n ≤ N, u n ∈ U
Full source
theorem inf_map_atBot_neBot_iff : NeBotNeBot (F ⊓ map u atBot) ↔ ∀ U ∈ F, ∀ N, ∃ n ≤ N, u n ∈ U :=
inf_map_atTop_neBot_iff (α := αᵒᵈ)Informal description
For a filter $F$ on a type $\beta$ and a function $u : \alpha \to \beta$, the filter $F \sqcap \text{map } u \text{ atBot}$ is non-trivial if and only if for every set $U \in F$ and every natural number $N$, there exists an $n \leq N$ such that $u(n) \in U$.
Filter.tendsto_atTop'
theorem
: Tendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s
Full source
theorem tendsto_atTop' : TendstoTendsto f atTop l ↔ ∀ s ∈ l, ∃ a, ∀ b ≥ a, f b ∈ s := by
simp only [tendsto_def, mem_atTop_sets, mem_preimage]Informal description
A function $f : \alpha \to \beta$ tends to a filter $l$ along the `atTop` filter if and only if for every set $s$ in $l$, there exists an element $a \in \alpha$ such that for all $b \geq a$, $f(b) \in s$.
Filter.tendsto_atTop_principal
theorem
{s : Set β} : Tendsto f atTop (𝓟 s) ↔ ∃ N, ∀ n ≥ N, f n ∈ s
Informal description
For a function $f : \alpha \to \beta$ and a set $s \subseteq \beta$, the function $f$ tends to $s$ along the filter `atTop` if and only if there exists a natural number $N$ such that for all $n \geq N$, $f(n) \in s$.
Filter.tendsto_atTop_atTop
theorem
: Tendsto f atTop atTop ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → b ≤ f a
Full source
/-- A function `f` grows to `+∞` independent of an order-preserving embedding `e`. -/
theorem tendsto_atTop_atTop : TendstoTendsto f atTop atTop ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → b ≤ f a :=
tendsto_iInf.trans <| forall_congr' fun _ => tendsto_atTop_principalInformal description
A function $f : \alpha \to \beta$ tends to $+\infty$ along the filter `atTop` (i.e., $f \to +\infty$ as $x \to +\infty$) if and only if for every element $b \in \beta$, there exists an index $i \in \alpha$ such that for all $a \geq i$, $b \leq f(a)$.
Filter.tendsto_atTop_atBot
theorem
: Tendsto f atTop atBot ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → f a ≤ b
Full source
theorem tendsto_atTop_atBot : TendstoTendsto f atTop atBot ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → f a ≤ b :=
tendsto_atTop_atTop (β := βᵒᵈ)Informal description
A function $f : \alpha \to \beta$ tends to $-\infty$ along the filter `atTop` (i.e., $f \to -\infty$ as $x \to +\infty$) if and only if for every element $b \in \beta$, there exists an index $i \in \alpha$ such that for all $a \geq i$, $f(a) \leq b$.
Filter.tendsto_atTop_atTop_iff_of_monotone
theorem
(hf : Monotone f) : Tendsto f atTop atTop ↔ ∀ b : β, ∃ a, b ≤ f a
Full source
theorem tendsto_atTop_atTop_iff_of_monotone (hf : Monotone f) :
TendstoTendsto f atTop atTop ↔ ∀ b : β, ∃ a, b ≤ f a :=
tendsto_atTop_atTop.trans <| forall_congr' fun _ => exists_congr fun a =>
⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans h <| hf ha'⟩Informal description
Let $f : \alpha \to \beta$ be a monotone function between preorders. Then $f$ tends to $+\infty$ along the `atTop` filter (i.e., $f(x) \to +\infty$ as $x \to +\infty$) if and only if for every $b \in \beta$, there exists $a \in \alpha$ such that $b \leq f(a)$.
Filter.tendsto_atTop_atBot_iff_of_antitone
theorem
(hf : Antitone f) : Tendsto f atTop atBot ↔ ∀ b : β, ∃ a, f a ≤ b
Full source
theorem tendsto_atTop_atBot_iff_of_antitone (hf : Antitone f) :
TendstoTendsto f atTop atBot ↔ ∀ b : β, ∃ a, f a ≤ b :=
tendsto_atTop_atTop_iff_of_monotone (β := βᵒᵈ) hfInformal description
Let $f : \alpha \to \beta$ be an antitone function between preorders. Then $f$ tends to $-\infty$ along the `atTop` filter (i.e., $f(x) \to -\infty$ as $x \to +\infty$) if and only if for every $b \in \beta$, there exists $a \in \alpha$ such that $f(a) \leq b$.
Filter.tendsto_atBot'
theorem
: Tendsto f atBot l ↔ ∀ s ∈ l, ∃ a, ∀ b ≤ a, f b ∈ s
Full source
theorem tendsto_atBot' : TendstoTendsto f atBot l ↔ ∀ s ∈ l, ∃ a, ∀ b ≤ a, f b ∈ s :=
tendsto_atTop' (α := αᵒᵈ)Informal description
A function $f : \alpha \to \beta$ tends to a filter $l$ along the `atBot` filter if and only if for every set $s$ in $l$, there exists an element $a \in \alpha$ such that for all $b \leq a$, $f(b) \in s$.
Filter.tendsto_atBot_principal
theorem
{s : Set β} : Tendsto f atBot (𝓟 s) ↔ ∃ N, ∀ n ≤ N, f n ∈ s
Full source
theorem tendsto_atBot_principal {s : Set β} : TendstoTendsto f atBot (𝓟 s) ↔ ∃ N, ∀ n ≤ N, f n ∈ s :=
tendsto_atTop_principal (α := αᵒᵈ) (β := βᵒᵈ)Informal description
For a function $f : \alpha \to \beta$ and a set $s \subseteq \beta$, the function $f$ tends to $s$ along the filter `atBot` if and only if there exists an element $N \in \alpha$ such that for all $n \leq N$, $f(n) \in s$.
Filter.tendsto_atBot_atTop
theorem
: Tendsto f atBot atTop ↔ ∀ b : β, ∃ i : α, ∀ a : α, a ≤ i → b ≤ f a
Full source
theorem tendsto_atBot_atTop : TendstoTendsto f atBot atTop ↔ ∀ b : β, ∃ i : α, ∀ a : α, a ≤ i → b ≤ f a :=
tendsto_atTop_atTop (α := αᵒᵈ)Informal description
A function $f : \alpha \to \beta$ between preorders tends to $+\infty$ along the `atBot` filter (i.e., $f(x) \to +\infty$ as $x \to -\infty$) if and only if for every $b \in \beta$, there exists an index $i \in \alpha$ such that for all $a \leq i$, we have $b \leq f(a)$.
Filter.tendsto_atBot_atBot
theorem
: Tendsto f atBot atBot ↔ ∀ b : β, ∃ i : α, ∀ a : α, a ≤ i → f a ≤ b
Full source
theorem tendsto_atBot_atBot : TendstoTendsto f atBot atBot ↔ ∀ b : β, ∃ i : α, ∀ a : α, a ≤ i → f a ≤ b :=
tendsto_atTop_atTop (α := αᵒᵈ) (β := βᵒᵈ)Informal description
A function $f : \alpha \to \beta$ tends to $-\infty$ along the filter `atBot` (i.e., $f \to -\infty$ as $x \to -\infty$) if and only if for every element $b \in \beta$, there exists an index $i \in \alpha$ such that for all $a \leq i$, $f(a) \leq b$.
Filter.tendsto_atBot_atBot_iff_of_monotone
theorem
(hf : Monotone f) : Tendsto f atBot atBot ↔ ∀ b : β, ∃ a, f a ≤ b
Full source
theorem tendsto_atBot_atBot_iff_of_monotone (hf : Monotone f) :
TendstoTendsto f atBot atBot ↔ ∀ b : β, ∃ a, f a ≤ b :=
tendsto_atBot_atBot.trans <| forall_congr' fun _ => exists_congr fun a =>
⟨fun h => h a (le_refl a), fun h _a' ha' => le_trans (hf ha') h⟩Informal description
Let $f : \alpha \to \beta$ be a monotone function between preorders. Then $f$ tends to $-\infty$ along the `atBot` filter (i.e., $f(x) \to -\infty$ as $x \to -\infty$) if and only if for every $b \in \beta$, there exists $a \in \alpha$ such that $f(a) \leq b$.
Filter.tendsto_atBot_atTop_iff_of_antitone
theorem
(hf : Antitone f) : Tendsto f atBot atTop ↔ ∀ b : β, ∃ a, b ≤ f a
Full source
theorem tendsto_atBot_atTop_iff_of_antitone (hf : Antitone f) :
TendstoTendsto f atBot atTop ↔ ∀ b : β, ∃ a, b ≤ f a :=
tendsto_atBot_atBot_iff_of_monotone (β := βᵒᵈ) hfInformal description
Let $f : \alpha \to \beta$ be an antitone function between preorders. Then $f$ tends to $+\infty$ along the `atBot` filter (i.e., $f(x) \to +\infty$ as $x \to -\infty$) if and only if for every $b \in \beta$, there exists $a \in \alpha$ such that $b \leq f(a)$.
Filter.Tendsto.subseq_mem
theorem
{F : Filter α} {V : ℕ → Set α} (h : ∀ n, V n ∈ F) {u : ℕ → α} (hu : Tendsto u atTop F) :
∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, u (φ n) ∈ V n
Full source
theorem Tendsto.subseq_mem {F : Filter α} {V : ℕ → Set α} (h : ∀ n, V n ∈ F) {u : ℕ → α}
(hu : Tendsto u atTop F) : ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, u (φ n) ∈ V n :=
extraction_forall_of_eventually'
(fun n => tendsto_atTop'.mp hu _ (h n) : ∀ n, ∃ N, ∀ k ≥ N, u k ∈ V n)Informal description
Let $F$ be a filter on a type $\alpha$, and let $(V_n)_{n \in \mathbb{N}}$ be a sequence of sets in $F$. Given a sequence $(u_n)_{n \in \mathbb{N}}$ in $\alpha$ that tends to $F$ along the `atTop` filter, there exists a strictly increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that for all $n \in \mathbb{N}$, the term $u_{\varphi(n)}$ belongs to $V_n$.
Filter.map_atTop_eq_of_gc_preorder
theorem
[Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β} (hf : Monotone f) (b : β)
(hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ a, f a ≤ c ↔ a ≤ x) : map f atTop = atTop
Full source
/-- A function `f` maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above `b`. -/
theorem map_atTop_eq_of_gc_preorder
[Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] [IsDirected β (· ≤ ·)] {f : α → β}
(hf : Monotone f) (b : β)
(hgi : ∀ c ≥ b, ∃ x, f x = c ∧ ∀ a, f a ≤ c ↔ a ≤ x) : map f atTop = atTop := by
have : Nonempty α := (hgi b le_rfl).nonempty
choose! g hfg hgle using hgi
refine le_antisymm (hf.tendsto_atTop_atTop fun c ↦ ?_) ?_
· rcases exists_ge_ge c b with ⟨d, hcd, hbd⟩
exact ⟨g d, hcd.trans (hfg d hbd).ge⟩
· have : Nonempty α := ⟨g b⟩
rw [(atTop_basis.map f).ge_iff]
intro a _
filter_upwards [eventually_ge_atTop (f a), eventually_ge_atTop b] with c hac hbc
exact ⟨g c, (hgle _ hbc _).1 hac, hfg _ hbc⟩Informal description
Let $\alpha$ and $\beta$ be preorders that are directed with respect to the $\leq$ relation. Given a monotone function $f : \alpha \to \beta$ and an element $b \in \beta$, suppose that for every $c \geq b$, there exists $x \in \alpha$ such that $f(x) = c$ and for all $a \in \alpha$, $f(a) \leq c$ if and only if $a \leq x$. Then the image of the `atTop` filter under $f$ is equal to the `atTop` filter on $\beta$.
Filter.map_atTop_eq_of_gc
theorem
[Preorder α] [IsDirected α (· ≤ ·)] [PartialOrder β] [IsDirected β (· ≤ ·)] {f : α → β} (g : β → α) (b : β)
(hf : Monotone f) (gc : ∀ a, ∀ c ≥ b, f a ≤ c ↔ a ≤ g c) (hgi : ∀ c ≥ b, c ≤ f (g c)) : map f atTop = atTop
Full source
/-- A function `f` maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above `b`. -/
theorem map_atTop_eq_of_gc
[Preorder α] [IsDirected α (· ≤ ·)] [PartialOrder β] [IsDirected β (· ≤ ·)]
{f : α → β} (g : β → α) (b : β) (hf : Monotone f)
(gc : ∀ a, ∀ c ≥ b, f a ≤ c ↔ a ≤ g c) (hgi : ∀ c ≥ b, c ≤ f (g c)) :
map f atTop = atTop :=
map_atTop_eq_of_gc_preorder hf b fun c hc ↦
⟨g c, le_antisymm ((gc _ _ hc).2 le_rfl) (hgi c hc), (gc · c hc)⟩Informal description
Let $\alpha$ and $\beta$ be preorders that are directed with respect to the $\leq$ relation, with $\beta$ being a partial order. Given a monotone function $f : \alpha \to \beta$ and a function $g : \beta \to \alpha$ such that for all $a \in \alpha$ and $c \geq b$ in $\beta$, the inequality $f(a) \leq c$ holds if and only if $a \leq g(c)$, and for all $c \geq b$, $c \leq f(g(c))$, then the image of the `atTop` filter under $f$ is equal to the `atTop` filter on $\beta$.
Filter.map_atBot_eq_of_gc_preorder
theorem
[Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] [IsDirected β (· ≥ ·)] {f : α → β} (hf : Monotone f) (b : β)
(hgi : ∀ c ≤ b, ∃ x, f x = c ∧ ∀ a, c ≤ f a ↔ x ≤ a) : map f atBot = atBot
Full source
theorem map_atBot_eq_of_gc_preorder
[Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] [IsDirected β (· ≥ ·)] {f : α → β}
(hf : Monotone f) (b : β)
(hgi : ∀ c ≤ b, ∃ x, f x = c ∧ ∀ a, c ≤ f a ↔ x ≤ a) : map f atBot = atBot :=
map_atTop_eq_of_gc_preorder (α := αᵒᵈ) (β := βᵒᵈ) hf.dual _ hgiInformal description
Let $\alpha$ and $\beta$ be preorders that are directed with respect to the $\geq$ relation. Given a monotone function $f : \alpha \to \beta$ and an element $b \in \beta$, suppose that for every $c \leq b$, there exists $x \in \alpha$ such that $f(x) = c$ and for all $a \in \alpha$, $c \leq f(a)$ if and only if $x \leq a$. Then the image of the `atBot` filter under $f$ is equal to the `atBot` filter on $\beta$.
Filter.map_atBot_eq_of_gc
theorem
[Preorder α] [IsDirected α (· ≥ ·)] [PartialOrder β] [IsDirected β (· ≥ ·)] {f : α → β} (g : β → α) (b' : β)
(hf : Monotone f) (gc : ∀ a, ∀ b ≤ b', b ≤ f a ↔ g b ≤ a) (hgi : ∀ b ≤ b', f (g b) ≤ b) : map f atBot = atBot
Full source
theorem map_atBot_eq_of_gc [Preorder α] [IsDirected α (· ≥ ·)]
[PartialOrder β] [IsDirected β (· ≥ ·)] {f : α → β} (g : β → α) (b' : β)
(hf : Monotone f) (gc : ∀ a, ∀ b ≤ b', b ≤ f a ↔ g b ≤ a) (hgi : ∀ b ≤ b', f (g b) ≤ b) :
map f atBot = atBot :=
map_atTop_eq_of_gc (α := αᵒᵈ) (β := βᵒᵈ) _ _ hf.dual gc hgiInformal description
Let $\alpha$ and $\beta$ be preorders that are directed with respect to the $\geq$ relation, with $\beta$ being a partial order. Given a monotone function $f : \alpha \to \beta$ and a function $g : \beta \to \alpha$ such that for all $a \in \alpha$ and $b \leq b'$ in $\beta$, the inequality $b \leq f(a)$ holds if and only if $g(b) \leq a$, and for all $b \leq b'$, $f(g(b)) \leq b$, then the image of the `atBot` filter under $f$ is equal to the `atBot` filter on $\beta$.
Filter.map_val_atTop_of_Ici_subset
theorem
[Preorder α] [IsDirected α (· ≤ ·)] {a : α} {s : Set α} (h : Ici a ⊆ s) : map ((↑) : s → α) atTop = atTop
Full source
theorem map_val_atTop_of_Ici_subset [Preorder α] [IsDirected α (· ≤ ·)] {a : α} {s : Set α}
(h : IciIci a ⊆ s) : map ((↑) : s → α) atTop = atTop := by
choose f hl hr using exists_ge_ge (α := α)
have : DirectedOn (· ≤ ·) s := fun x _ y _ ↦
⟨f a (f x y), h <| hl _ _, (hl x y).trans (hr _ _), (hr x y).trans (hr _ _)⟩
have : IsDirected s (· ≤ ·) := by
rw [directedOn_iff_directed] at this
rwa [← directed_id_iff]
refine map_atTop_eq_of_gc_preorder (Subtype.mono_coe _) a fun c hc ↦ ?_
exact ⟨⟨c, h hc⟩, rfl, fun _ ↦ .rfl⟩Informal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$, and let $s$ be a subset of $\alpha$ containing the interval $[a, \infty)$ for some $a \in \alpha$. Then the image of the `atTop` filter under the inclusion map $\iota : s \to \alpha$ is equal to the `atTop` filter on $\alpha$.
Nat.map_cast_int_atTop
theorem
: map ((↑) : ℕ → ℤ) atTop = atTop
Full source
@[simp]
theorem _root_.Nat.map_cast_int_atTop : map ((↑) : ℕ → ℤ) atTop = atTop := by
refine map_atTop_eq_of_gc_preorder (fun _ _ ↦ Int.ofNat_le.2) 0 fun n hn ↦ ?_
lift n to ℕ using hn
exact ⟨n, rfl, fun _ ↦ Int.ofNat_le⟩Informal description
The image of the `atTop` filter on natural numbers under the canonical embedding from $\mathbb{N}$ to $\mathbb{Z}$ is equal to the `atTop` filter on $\mathbb{Z}$.
Filter.map_val_Ici_atTop
theorem
[Preorder α] [IsDirected α (· ≤ ·)] (a : α) : map ((↑) : Ici a → α) atTop = atTop
Full source
/-- The image of the filter `atTop` on `Ici a` under the coercion equals `atTop`. -/
@[simp]
theorem map_val_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)] (a : α) :
map ((↑) : Ici a → α) atTop = atTop :=
map_val_atTop_of_Ici_subset Subset.rflInformal description
Let $\alpha$ be a directed preorder and $a \in \alpha$. The image of the `atTop` filter on the interval $[a, \infty)$ under the inclusion map $\iota : [a, \infty) \to \alpha$ is equal to the `atTop` filter on $\alpha$.
Filter.map_val_Ioi_atTop
theorem
[Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α] (a : α) : map ((↑) : Ioi a → α) atTop = atTop
Full source
/-- The image of the filter `atTop` on `Ioi a` under the coercion equals `atTop`. -/
@[simp]
theorem map_val_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α] (a : α) :
map ((↑) : Ioi a → α) atTop = atTop :=
let ⟨_b, hb⟩ := exists_gt a
map_val_atTop_of_Ici_subset <| Ici_subset_Ioi.2 hbInformal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$ and has no maximal elements. For any element $a \in \alpha$, the image of the `atTop` filter on the open interval $(a, \infty)$ under the inclusion map $\iota : (a, \infty) \to \alpha$ is equal to the `atTop` filter on $\alpha$.
Filter.atTop_Ioi_eq
theorem
[Preorder α] [IsDirected α (· ≤ ·)] (a : α) : atTop = comap ((↑) : Ioi a → α) atTop
Full source
/-- The `atTop` filter for an open interval `Ioi a` comes from the `atTop` filter in the ambient
order. -/
theorem atTop_Ioi_eq [Preorder α] [IsDirected α (· ≤ ·)] (a : α) :
atTop = comap ((↑) : Ioi a → α) atTop := by
rcases isEmpty_or_nonempty (Ioi a) with h|⟨⟨b, hb⟩⟩
· subsingleton
· rw [← map_val_atTop_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map Subtype.coe_injective]Informal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$, and let $a \in \alpha$. The filter `atTop` on $\alpha$ is equal to the preimage of the `atTop` filter under the inclusion map $\iota : (a, \infty) \to \alpha$.
Filter.atTop_Ici_eq
theorem
[Preorder α] [IsDirected α (· ≤ ·)] (a : α) : atTop = comap ((↑) : Ici a → α) atTop
Full source
/-- The `atTop` filter for an open interval `Ici a` comes from the `atTop` filter in the ambient
order. -/
theorem atTop_Ici_eq [Preorder α] [IsDirected α (· ≤ ·)] (a : α) :
atTop = comap ((↑) : Ici a → α) atTop := by
rw [← map_val_Ici_atTop a, comap_map Subtype.coe_injective]Informal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$, and let $a \in \alpha$. The `atTop` filter on $\alpha$ is equal to the preimage of the `atTop` filter under the inclusion map $\iota : [a, \infty) \to \alpha$.
Filter.map_val_Iio_atBot
theorem
[Preorder α] [IsDirected α (· ≥ ·)] [NoMinOrder α] (a : α) : map ((↑) : Iio a → α) atBot = atBot
Full source
/-- The `atBot` filter for an open interval `Iio a` comes from the `atBot` filter in the ambient
order. -/
@[simp]
theorem map_val_Iio_atBot [Preorder α] [IsDirected α (· ≥ ·)] [NoMinOrder α] (a : α) :
map ((↑) : Iio a → α) atBot = atBot :=
map_val_Ioi_atTop (OrderDual.toDual a)Informal description
Let $\alpha$ be a preorder that is directed with respect to $\geq$ and has no minimal elements. For any element $a \in \alpha$, the image of the `atBot` filter on the open interval $(-\infty, a)$ under the inclusion map $\iota : (-\infty, a) \to \alpha$ is equal to the `atBot` filter on $\alpha$.
Filter.atBot_Iio_eq
theorem
[Preorder α] [IsDirected α (· ≥ ·)] (a : α) : atBot = comap ((↑) : Iio a → α) atBot
Full source
/-- The `atBot` filter for an open interval `Iio a` comes from the `atBot` filter in the ambient
order. -/
theorem atBot_Iio_eq [Preorder α] [IsDirected α (· ≥ ·)] (a : α) :
atBot = comap ((↑) : Iio a → α) atBot :=
atTop_Ioi_eq (OrderDual.toDual a)Informal description
Let $\alpha$ be a preorder that is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound). For any element $a \in \alpha$, the filter `atBot` on $\alpha$ is equal to the preimage of the `atBot` filter under the inclusion map $\iota : (-\infty, a) \to \alpha$.
Filter.map_val_Iic_atBot
theorem
[Preorder α] [IsDirected α (· ≥ ·)] (a : α) : map ((↑) : Iic a → α) atBot = atBot
Full source
/-- The `atBot` filter for an open interval `Iic a` comes from the `atBot` filter in the ambient
order. -/
@[simp]
theorem map_val_Iic_atBot [Preorder α] [IsDirected α (· ≥ ·)] (a : α) :
map ((↑) : Iic a → α) atBot = atBot :=
map_val_Ici_atTop (OrderDual.toDual a)Informal description
Let $\alpha$ be a preordered set directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound). For any element $a \in \alpha$, the image of the `atBot` filter on the left-infinite right-closed interval $(-\infty, a]$ under the inclusion map $\iota : (-\infty, a] \to \alpha$ is equal to the `atBot` filter on $\alpha$.
Filter.atBot_Iic_eq
theorem
[Preorder α] [IsDirected α (· ≥ ·)] (a : α) : atBot = comap ((↑) : Iic a → α) atBot
Full source
/-- The `atBot` filter for an open interval `Iic a` comes from the `atBot` filter in the ambient
order. -/
theorem atBot_Iic_eq [Preorder α] [IsDirected α (· ≥ ·)] (a : α) :
atBot = comap ((↑) : Iic a → α) atBot :=
atTop_Ici_eq (OrderDual.toDual a)Informal description
Let $\alpha$ be a preorder that is directed with respect to the relation $\geq$ (i.e., every pair of elements has a common lower bound). For any element $a \in \alpha$, the `atBot` filter on $\alpha$ is equal to the preimage of the `atBot` filter under the inclusion map $\iota : (-\infty, a] \to \alpha$.
Filter.tendsto_Ioi_atTop
theorem
[Preorder α] [IsDirected α (· ≤ ·)] {a : α} {f : β → Ioi a} {l : Filter β} :
Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop
Full source
theorem tendsto_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)]
{a : α} {f : β → Ioi a} {l : Filter β} :
TendstoTendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop := by
rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]Informal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$, and let $a \in \alpha$. For a function $f : \beta \to (a, \infty)$ and a filter $l$ on $\beta$, the following are equivalent:
1. The function $f$ tends to the `atTop` filter on $(a, \infty)$ with respect to $l$.
2. The composition of $f$ with the inclusion map $(a, \infty) \hookrightarrow \alpha$ tends to the `atTop` filter on $\alpha$ with respect to $l$.
In other words, $f$ tends to infinity in $(a, \infty)$ if and only if its image in $\alpha$ tends to infinity.
Filter.tendsto_Iio_atBot
theorem
[Preorder α] [IsDirected α (· ≥ ·)] {a : α} {f : β → Iio a} {l : Filter β} :
Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l atBot
Full source
theorem tendsto_Iio_atBot [Preorder α] [IsDirected α (· ≥ ·)]
{a : α} {f : β → Iio a} {l : Filter β} :
TendstoTendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l atBot :=
tendsto_Ioi_atTop (α := αᵒᵈ)Informal description
Let $\alpha$ be a preorder that is directed with respect to $\geq$, and let $a \in \alpha$. For a function $f : \beta \to (-\infty, a)$ and a filter $l$ on $\beta$, the following are equivalent:
1. The function $f$ tends to the `atBot` filter on $(-\infty, a)$ with respect to $l$.
2. The composition of $f$ with the inclusion map $(-\infty, a) \hookrightarrow \alpha$ tends to the `atBot` filter on $\alpha$ with respect to $l$.
In other words, $f$ tends to negative infinity in $(-\infty, a)$ if and only if its image in $\alpha$ tends to negative infinity.
Filter.tendsto_Ici_atTop
theorem
[Preorder α] [IsDirected α (· ≤ ·)] {a : α} {f : β → Ici a} {l : Filter β} :
Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop
Full source
theorem tendsto_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)]
{a : α} {f : β → Ici a} {l : Filter β} :
TendstoTendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop := by
rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]Informal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$, and let $a \in \alpha$. For a function $f : \beta \to [a, \infty)$ and a filter $l$ on $\beta$, the following are equivalent:
1. The function $f$ tends to the `atTop` filter on $[a, \infty)$ with respect to $l$.
2. The composition of $f$ with the inclusion map $[a, \infty) \hookrightarrow \alpha$ tends to the `atTop` filter on $\alpha$ with respect to $l$.
In other words, $f$ tends to infinity in $[a, \infty)$ if and only if its image in $\alpha$ tends to infinity.
Filter.tendsto_Iic_atBot
theorem
[Preorder α] [IsDirected α (· ≥ ·)] {a : α} {f : β → Iic a} {l : Filter β} :
Tendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l atBot
Full source
theorem tendsto_Iic_atBot [Preorder α] [IsDirected α (· ≥ ·)]
{a : α} {f : β → Iic a} {l : Filter β} :
TendstoTendsto f l atBot ↔ Tendsto (fun x => (f x : α)) l atBot :=
tendsto_Ici_atTop (α := αᵒᵈ)Informal description
Let $\alpha$ be a preorder that is directed with respect to $\geq$, and let $a \in \alpha$. For a function $f : \beta \to (-\infty, a]$ and a filter $l$ on $\beta$, the following are equivalent:
1. The function $f$ tends to the `atBot` filter on $(-\infty, a]$ with respect to $l$.
2. The composition of $f$ with the inclusion map $(-\infty, a] \hookrightarrow \alpha$ tends to the `atBot` filter on $\alpha$ with respect to $l$.
Filter.tendsto_comp_val_Ioi_atTop
theorem
[Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun x : Ioi a => f x) atTop l ↔ Tendsto f atTop l
Full source
@[simp]
theorem tendsto_comp_val_Ioi_atTop [Preorder α] [IsDirected α (· ≤ ·)] [NoMaxOrder α]
{a : α} {f : α → β} {l : Filter β} :
TendstoTendsto (fun x : Ioi a => f x) atTop l ↔ Tendsto f atTop l := by
rw [← map_val_Ioi_atTop a, tendsto_map'_iff, Function.comp_def]Informal description
Let $\alpha$ be a preorder that is directed with respect to $\leq$ and has no maximal elements. For any element $a \in \alpha$ and any function $f : \alpha \to \beta$, the composition $f \circ \iota$ tends to a filter $l$ along the `atTop` filter on the open interval $(a, \infty)$ if and only if $f$ tends to $l$ along the `atTop` filter on $\alpha$, where $\iota : (a, \infty) \to \alpha$ is the inclusion map.
Filter.tendsto_comp_val_Ici_atTop
theorem
[Preorder α] [IsDirected α (· ≤ ·)] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun x : Ici a => f x) atTop l ↔ Tendsto f atTop l
Full source
@[simp]
theorem tendsto_comp_val_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)]
{a : α} {f : α → β} {l : Filter β} :
TendstoTendsto (fun x : Ici a => f x) atTop l ↔ Tendsto f atTop l := by
rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]Informal description
Let $\alpha$ be a directed preorder and $\beta$ a type. For any function $f \colon \alpha \to \beta$, any filter $l$ on $\beta$, and any element $a \in \alpha$, the following are equivalent:
1. The composition of $f$ with the inclusion map $\iota \colon [a, \infty) \to \alpha$ tends to $l$ along the `atTop` filter on $[a, \infty)$.
2. The function $f$ tends to $l$ along the `atTop` filter on $\alpha$.
Filter.tendsto_comp_val_Iio_atBot
theorem
[Preorder α] [IsDirected α (· ≥ ·)] [NoMinOrder α] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun x : Iio a => f x) atBot l ↔ Tendsto f atBot l
Full source
@[simp]
theorem tendsto_comp_val_Iio_atBot [Preorder α] [IsDirected α (· ≥ ·)] [NoMinOrder α]
{a : α} {f : α → β} {l : Filter β} :
TendstoTendsto (fun x : Iio a => f x) atBot l ↔ Tendsto f atBot l :=
tendsto_comp_val_Ioi_atTop (α := αᵒᵈ)Informal description
Let $\alpha$ be a preorder that is directed with respect to $\geq$ and has no minimal elements. For any element $a \in \alpha$, any function $f : \alpha \to \beta$, and any filter $l$ on $\beta$, the composition $f \circ \iota$ tends to $l$ along the `atBot` filter on the open interval $(-\infty, a)$ if and only if $f$ tends to $l$ along the `atBot` filter on $\alpha$, where $\iota : (-\infty, a) \to \alpha$ is the inclusion map.
Filter.tendsto_comp_val_Iic_atBot
theorem
[Preorder α] [IsDirected α (· ≥ ·)] {a : α} {f : α → β} {l : Filter β} :
Tendsto (fun x : Iic a => f x) atBot l ↔ Tendsto f atBot l
Full source
@[simp]
theorem tendsto_comp_val_Iic_atBot [Preorder α] [IsDirected α (· ≥ ·)]
{a : α} {f : α → β} {l : Filter β} :
TendstoTendsto (fun x : Iic a => f x) atBot l ↔ Tendsto f atBot l :=
tendsto_comp_val_Ici_atTop (α := αᵒᵈ)Informal description
Let $\alpha$ be a preorder directed with respect to $\geq$ (i.e., every pair of elements has a common lower bound), $\beta$ a type, $a \in \alpha$, $f \colon \alpha \to \beta$ a function, and $l$ a filter on $\beta$. Then the following are equivalent:
1. The composition of $f$ with the inclusion map $\iota \colon (-\infty, a] \to \alpha$ tends to $l$ along the `atBot` filter on $(-\infty, a]$.
2. The function $f$ tends to $l$ along the `atBot` filter on $\alpha$.
Filter.map_add_atTop_eq_nat
theorem
(k : ℕ) : map (fun a => a + k) atTop = atTop
Full source
theorem map_add_atTop_eq_nat (k : ℕ) : map (fun a => a + k) atTop = atTop :=
map_atTop_eq_of_gc (· - k) k (fun _ _ h => Nat.add_le_add_right h k)
(fun _ _ h => (Nat.le_sub_iff_add_le h).symm) fun a h => by rw [Nat.sub_add_cancel h]Informal description
For any natural number $k$, the image of the `atTop` filter under the function $a \mapsto a + k$ is equal to the `atTop` filter itself. In other words, the filter of sets containing all sufficiently large natural numbers is preserved under addition by a constant $k$.
Filter.map_sub_atTop_eq_nat
theorem
(k : ℕ) : map (fun a => a - k) atTop = atTop
Full source
theorem map_sub_atTop_eq_nat (k : ℕ) : map (fun a => a - k) atTop = atTop :=
map_atTop_eq_of_gc (· + k) 0 (fun _ _ h => Nat.sub_le_sub_right h _)
(fun _ _ _ => Nat.sub_le_iff_le_add) fun b _ => by rw [Nat.add_sub_cancel_right]Informal description
For any natural number $k$, the image of the `atTop` filter under the function $a \mapsto a - k$ is equal to the `atTop` filter itself. In other words, the filter of sets containing all sufficiently large natural numbers is preserved under subtraction by a constant $k$.
Filter.tendsto_add_atTop_nat
theorem
(k : ℕ) : Tendsto (fun a => a + k) atTop atTop
Full source
theorem tendsto_add_atTop_nat (k : ℕ) : Tendsto (fun a => a + k) atTop atTop :=
le_of_eq (map_add_atTop_eq_nat k)Informal description
For any natural number $k$, the function $f(a) = a + k$ tends to infinity as $a$ tends to infinity. In other words, the sequence $(a + k)_{a \in \mathbb{N}}$ diverges to $+\infty$ as $a \to +\infty$.
Filter.tendsto_sub_atTop_nat
theorem
(k : ℕ) : Tendsto (fun a => a - k) atTop atTop
Full source
theorem tendsto_sub_atTop_nat (k : ℕ) : Tendsto (fun a => a - k) atTop atTop :=
le_of_eq (map_sub_atTop_eq_nat k)Informal description
For any natural number $k$, the function $f(a) = a - k$ tends to infinity as $a$ tends to infinity. In other words, the sequence $(a - k)_{a \in \mathbb{N}}$ diverges to $+\infty$ as $a \to +\infty$.
Filter.tendsto_add_atTop_iff_nat
theorem
{f : ℕ → α} {l : Filter α} (k : ℕ) : Tendsto (fun n => f (n + k)) atTop l ↔ Tendsto f atTop l
Full source
theorem tendsto_add_atTop_iff_nat {f : ℕ → α} {l : Filter α} (k : ℕ) :
TendstoTendsto (fun n => f (n + k)) atTop l ↔ Tendsto f atTop l :=
show TendstoTendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l by
rw [← tendsto_map'_iff, map_add_atTop_eq_nat]Informal description
For any function $f \colon \mathbb{N} \to \alpha$ and any filter $l$ on $\alpha$, the function $n \mapsto f(n + k)$ tends to $l$ as $n \to \infty$ if and only if $f$ tends to $l$ as $n \to \infty$.
Filter.map_div_atTop_eq_nat
theorem
(k : ℕ) (hk : 0 < k) : map (fun a => a / k) atTop = atTop
Full source
theorem map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) : map (fun a => a / k) atTop = atTop :=
map_atTop_eq_of_gc (fun b => k * b + (k - 1)) 1 (fun _ _ h => Nat.div_le_div_right h)
(fun a b _ => by rw [Nat.div_le_iff_le_mul_add_pred hk])
fun b _ => by rw [Nat.mul_add_div hk, Nat.div_eq_of_lt, Nat.add_zero]; omegaInformal description
For any positive natural number $k > 0$, the image of the `atTop` filter under the function $a \mapsto \lfloor a / k \rfloor$ (natural number division) is equal to the `atTop` filter itself. In other words, the sequence $\lfloor n / k \rfloor$ tends to infinity as $n$ tends to infinity.
Filter.not_bddAbove_of_tendsto_atTop
theorem
[NoMaxOrder β] (h : Tendsto f l atTop) : ¬BddAbove (range f)
Full source
theorem not_bddAbove_of_tendsto_atTop [NoMaxOrder β] (h : Tendsto f l atTop) :
¬BddAbove (range f) := by
rintro ⟨M, hM⟩
have : ∀ x, f x ≤ M := by aesop
have : ∅ = f ⁻¹' Ioi M := by aesop (add forward safe not_le_of_lt)
apply Filter.empty_not_mem l
aesop (add safe Ioi_mem_atTop)Informal description
Let $\beta$ be a preorder with no maximal elements. If a function $f$ tends to positive infinity along a filter $l$ (i.e., $f \to +\infty$ as $l \to \infty$), then the range of $f$ is not bounded above in $\beta$.
Filter.not_bddBelow_of_tendsto_atBot
theorem
[NoMinOrder β] (h : Tendsto f l atBot) : ¬BddBelow (range f)
Full source
theorem not_bddBelow_of_tendsto_atBot [NoMinOrder β] (h : Tendsto f l atBot) :
¬BddBelow (range f) := not_bddAbove_of_tendsto_atTop (β := βᵒᵈ) hInformal description
Let $\beta$ be a preorder with no minimal elements. If a function $f$ tends to negative infinity along a filter $l$ (i.e., $f \to -\infty$ as $l \to \infty$), then the range of $f$ is not bounded below in $\beta$.
Filter.HasAntitoneBasis.eventually_subset
theorem
[Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {t : Set α} (ht : t ∈ l) :
∀ᶠ i in atTop, s i ⊆ t
Full source
theorem HasAntitoneBasis.eventually_subset [Preorder ι] {l : Filter α} {s : ι → Set α}
(hl : l.HasAntitoneBasis s) {t : Set α} (ht : t ∈ l) : ∀ᶠ i in atTop, s i ⊆ t :=
let ⟨i, _, hi⟩ := hl.1.mem_iff.1 ht
(eventually_ge_atTop i).mono fun _j hj => (hl.antitone hj).trans hiInformal description
Let $\iota$ be a preorder, $\alpha$ a type, and $l$ a filter on $\alpha$ with an antitone basis $s : \iota \to \text{Set} \alpha$. For any set $t \in l$, the basis sets $s(i)$ are eventually (with respect to the `atTop` filter on $\iota$) contained in $t$, i.e., $\forall^\infty i \text{ in } \text{atTop}, s(i) \subseteq t$.
Filter.HasAntitoneBasis.tendsto
theorem
[Preorder ι] {l : Filter α} {s : ι → Set α} (hl : l.HasAntitoneBasis s) {φ : ι → α} (h : ∀ i : ι, φ i ∈ s i) :
Tendsto φ atTop l
Full source
protected theorem HasAntitoneBasis.tendsto [Preorder ι] {l : Filter α} {s : ι → Set α}
(hl : l.HasAntitoneBasis s) {φ : ι → α} (h : ∀ i : ι, φ i ∈ s i) : Tendsto φ atTop l :=
fun _t ht => mem_map.2 <| (hl.eventually_subset ht).mono fun i hi => hi (h i)Informal description
Let $\iota$ be a preorder and $\alpha$ a type. Suppose $l$ is a filter on $\alpha$ with an antitone basis $s : \iota \to \text{Set} \alpha$, meaning $s$ is decreasing and $l$ is generated by the sets $s(i)$. If $\varphi : \iota \to \alpha$ is a function such that $\varphi(i) \in s(i)$ for all $i \in \iota$, then $\varphi$ tends to $l$ along the `atTop` filter on $\iota$.
Filter.HasAntitoneBasis.comp_mono
theorem
[Nonempty ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Preorder ι'] {l : Filter α} {s : ι' → Set α}
(hs : l.HasAntitoneBasis s) {φ : ι → ι'} (φ_mono : Monotone φ) (hφ : Tendsto φ atTop atTop) :
l.HasAntitoneBasis (s ∘ φ)
Full source
theorem HasAntitoneBasis.comp_mono [Nonempty ι] [Preorder ι] [IsDirected ι (· ≤ ·)] [Preorder ι']
{l : Filter α}
{s : ι' → Set α} (hs : l.HasAntitoneBasis s) {φ : ι → ι'} (φ_mono : Monotone φ)
(hφ : Tendsto φ atTop atTop) : l.HasAntitoneBasis (s ∘ φ) :=
⟨hs.1.to_hasBasis
(fun n _ => (hφ.eventually_ge_atTop n).exists.imp fun _m hm => ⟨trivial, hs.antitone hm⟩)
fun n _ => ⟨φ n, trivial, Subset.rfl⟩,
hs.antitone.comp_monotone φ_mono⟩Informal description
Let $\iota$ and $\iota'$ be nonempty preorders with $\iota$ directed. Suppose $l$ is a filter on a type $\alpha$ with an antitone basis $s : \iota' \to \text{Set} \alpha$, and $\varphi : \iota \to \iota'$ is a monotone function that tends to infinity (i.e., $\varphi(i) \to \infty$ as $i \to \infty$). Then the composition $s \circ \varphi : \iota \to \text{Set} \alpha$ also forms an antitone basis for $l$.
Filter.HasAntitoneBasis.comp_strictMono
theorem
{l : Filter α} {s : ℕ → Set α} (hs : l.HasAntitoneBasis s) {φ : ℕ → ℕ} (hφ : StrictMono φ) : l.HasAntitoneBasis (s ∘ φ)
Full source
theorem HasAntitoneBasis.comp_strictMono {l : Filter α} {s : ℕ → Set α} (hs : l.HasAntitoneBasis s)
{φ : ℕ → ℕ} (hφ : StrictMono φ) : l.HasAntitoneBasis (s ∘ φ) :=
hs.comp_mono hφ.monotone hφ.tendsto_atTopInformal description
Let $l$ be a filter on a type $\alpha$ with an antitone basis $s \colon \mathbb{N} \to \text{Set} \alpha$, and let $\varphi \colon \mathbb{N} \to \mathbb{N}$ be a strictly increasing function. Then the composition $s \circ \varphi$ also forms an antitone basis for $l$.
Filter.subseq_forall_of_frequently
theorem
{ι : Type*} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι} (h_tendsto : Tendsto x atTop l) (h : ∃ᶠ n in atTop, p (x n)) :
∃ ns : ℕ → ℕ, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ n, p (x (ns n))
Full source
theorem subseq_forall_of_frequently {ι : Type*} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι}
(h_tendsto : Tendsto x atTop l) (h : ∃ᶠ n in atTop, p (x n)) :
∃ ns : ℕ → ℕ, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ n, p (x (ns n)) := by
choose ns hge hns using frequently_atTop.1 h
exact ⟨ns, h_tendsto.comp (tendsto_atTop_mono hge tendsto_id), hns⟩Informal description
Let $\iota$ be a type, $x \colon \mathbb{N} \to \iota$ a sequence, $p \colon \iota \to \text{Prop}$ a predicate, and $l$ a filter on $\iota$. If $x$ tends to $l$ along the `atTop` filter on $\mathbb{N}$ and $p(x_n)$ holds frequently (i.e., for infinitely many $n$), then there exists a subsequence $x \circ \text{ns}$ of $x$ such that:
1. $x \circ \text{ns}$ tends to $l$ along `atTop`, and
2. $p(x(\text{ns}(n)))$ holds for all $n \in \mathbb{N}$.