Limits of Filter.atTop and Filter.atBot

In this file we prove many lemmas on the combination of Filter.atTop and Filter.atBot and Tendsto.

theorem Filter.not_tendsto_const_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [NoTopOrder α] (x : α) (l : Filter β) [l.NeBot] : ¬Tendsto (fun (x_1 : β) => x) l atTop

theorem Filter.not_tendsto_const_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [NoBotOrder α] (x : α) (l : Filter β) [l.NeBot] : ¬Tendsto (fun (x_1 : β) => x) l atBot

theorem Filter.Tendsto.eventually_gt_atTop {α : Type u_3} {β : Type u_4} [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : β) : ∀ᶠ (x : α) in l, c < f x

theorem Filter.Tendsto.eventually_ge_atTop {α : Type u_3} {β : Type u_4} [Preorder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : β) : ∀ᶠ (x : α) in l, c ≤ f x

theorem Filter.Tendsto.eventually_ne_atTop {α : Type u_3} {β : Type u_4} [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : β) : ∀ᶠ (x : α) in l, f x ≠ c

theorem Filter.Tendsto.eventually_ne_atTop' {α : Type u_3} {β : Type u_4} [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atTop) (c : α) : ∀ᶠ (x : α) in l, x ≠ c

theorem Filter.Tendsto.eventually_lt_atBot {α : Type u_3} {β : Type u_4} [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot) (c : β) : ∀ᶠ (x : α) in l, f x < c

theorem Filter.Tendsto.eventually_le_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot) (c : β) : ∀ᶠ (x : α) in l, f x ≤ c

theorem Filter.Tendsto.eventually_ne_atBot {α : Type u_3} {β : Type u_4} [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α} (hf : Tendsto f l atBot) (c : β) : ∀ᶠ (x : α) in l, f x ≠ c

theorem Filter.OrderTop.atTop_eq (α : Type u_6) [PartialOrder α] [OrderTop α] : atTop = pure ⊤

theorem Filter.OrderBot.atBot_eq (α : Type u_6) [PartialOrder α] [OrderBot α] : atBot = pure ⊥

theorem Filter.tendsto_atTop_pure {α : Type u_3} {β : Type u_4} [PartialOrder α] [OrderTop α] (f : α → β) : Tendsto f atTop (pure (f ⊤))

theorem Filter.tendsto_atBot_pure {α : Type u_3} {β : Type u_4} [PartialOrder α] [OrderBot α] (f : α → β) : Tendsto f atBot (pure (f ⊥))

theorem Filter.tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder β] {m : α → β} {f : Filter α} : Tendsto m f atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a

theorem Filter.tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {m : α → β} {f : Filter α} : Tendsto m f atBot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b

theorem Filter.tendsto_atTop_mono' {α : Type u_3} {β : Type u_4} [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂) (h₁ : Tendsto f₁ l atTop) : Tendsto f₂ l atTop

theorem Filter.tendsto_atBot_mono' {α : Type u_3} {β : Type u_4} [Preorder β] (l : Filter α) ⦃f₁ f₂ : α → β⦄ (h : f₁ ≤ᶠ[l] f₂) : Tendsto f₂ l atBot → Tendsto f₁ l atBot

theorem Filter.tendsto_atTop_mono {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ (n : α), f n ≤ g n) : Tendsto f l atTop → Tendsto g l atTop

theorem Filter.tendsto_atBot_mono {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ (n : α), f n ≤ g n) : Tendsto g l atBot → Tendsto f l atBot

Sequences

theorem StrictMono.tendsto_atTop {φ : ℕ → ℕ} (h : StrictMono φ) : Filter.Tendsto φ Filter.atTop Filter.atTop

theorem Monotone.upperBounds_range_comp_tendsto_atTop {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atTop) : upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)

If f is a monotone function and g tends to atTop along a nontrivial filter. then the upper bounds of the range of f ∘ g are the same as the upper bounds of the range of f.

This lemma together with exists_seq_monotone_tendsto_atTop_atTop below is useful to reduce a statement about a monotone family indexed by a type with countably generated atTop (e.g., ℝ) to the case of a family indexed by natural numbers.

theorem Monotone.lowerBounds_range_comp_tendsto_atBot {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atBot) : lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)

If f is a monotone function and g tends to atBot along a nontrivial filter. then the lower bounds of the range of f ∘ g are the same as the lower bounds of the range of f.

theorem Antitone.lowerBounds_range_comp_tendsto_atTop {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atTop) : lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)

If f is an antitone function and g tends to atTop along a nontrivial filter. then the upper bounds of the range of f ∘ g are the same as the upper bounds of the range of f.

theorem Antitone.upperBounds_range_comp_tendsto_atBot {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Filter.Tendsto g l Filter.atBot) : upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)

If f is an antitone function and g tends to atBot along a nontrivial filter. then the upper bounds of the range of f ∘ g are the same as the upper bounds of the range of f.

theorem Filter.tendsto_atTop_atTop_of_monotone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ (b : β), ∃ (a : α), b ≤ f a) : Tendsto f atTop atTop

theorem Filter.tendsto_atTop_atBot_of_antitone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) (h : ∀ (b : β), ∃ (a : α), f a ≤ b) : Tendsto f atTop atBot

theorem Filter.tendsto_atBot_atBot_of_monotone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ (b : β), ∃ (a : α), f a ≤ b) : Tendsto f atBot atBot

theorem Filter.tendsto_atBot_atTop_of_antitone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) (h : ∀ (b : β), ∃ (a : α), b ≤ f a) : Tendsto f atBot atTop

theorem Monotone.tendsto_atTop_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ (b : β), ∃ (a : α), b ≤ f a) : Filter.Tendsto f Filter.atTop Filter.atTop

Alias of Filter.tendsto_atTop_atTop_of_monotone.

theorem Monotone.tendsto_atBot_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) (h : ∀ (b : β), ∃ (a : α), f a ≤ b) : Filter.Tendsto f Filter.atBot Filter.atBot

Alias of Filter.tendsto_atBot_atBot_of_monotone.

theorem Filter.comap_embedding_atTop {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {e : β → γ} (hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ (c : γ), ∃ (b : β), c ≤ e b) : comap e atTop = atTop

theorem Filter.comap_embedding_atBot {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {e : β → γ} (hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ (c : γ), ∃ (b : β), e b ≤ c) : comap e atBot = atBot

theorem Filter.tendsto_atTop_embedding {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α} (hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ (c : γ), ∃ (b : β), c ≤ e b) : Tendsto (e ∘ f) l atTop ↔ Tendsto f l atTop

theorem Filter.tendsto_atBot_embedding {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] [Preorder γ] {f : α → β} {e : β → γ} {l : Filter α} (hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀ (c : γ), ∃ (b : β), e b ≤ c) : Tendsto (e ∘ f) l atBot ↔ Tendsto f l atBot

A function f goes to -∞ independent of an order-preserving embedding e.

theorem Filter.tendsto_atTop_atTop_of_monotone' {ι : Type u_1} {α : Type u_3} [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u) (H : ¬BddAbove (Set.range u)) : Tendsto u atTop atTop

If u is a monotone function with linear ordered codomain and the range of u is not bounded above, then Tendsto u atTop atTop.

theorem Filter.tendsto_atBot_atBot_of_monotone' {ι : Type u_1} {α : Type u_3} [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u) (H : ¬BddBelow (Set.range u)) : Tendsto u atBot atBot

If u is a monotone function with linear ordered codomain and the range of u is not bounded below, then Tendsto u atBot atBot.

theorem Filter.tendsto_atTop_of_monotone_of_filter {ι : Type u_1} {α : Type u_3} [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u) [l.NeBot] (hu : Tendsto u l atTop) : Tendsto u atTop atTop

If a monotone function u : ι → α tends to atTop along some non-trivial filter l, then it tends to atTop along atTop.

theorem Filter.tendsto_atBot_of_monotone_of_filter {ι : Type u_1} {α : Type u_3} [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u) [l.NeBot] (hu : Tendsto u l atBot) : Tendsto u atBot atBot

If a monotone function u : ι → α tends to atBot along some non-trivial filter l, then it tends to atBot along atBot.

theorem Filter.tendsto_atTop_of_monotone_of_subseq {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι} (h : Monotone u) {l : Filter ι'} [l.NeBot] (H : Tendsto (u ∘ φ) l atTop) : Tendsto u atTop atTop

theorem Filter.tendsto_atBot_of_monotone_of_subseq {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Preorder ι] [Preorder α] {u : ι → α} {φ : ι' → ι} (h : Monotone u) {l : Filter ι'} [l.NeBot] (H : Tendsto (u ∘ φ) l atBot) : Tendsto u atBot atBot