Filter.atTop and Filter.atBot filters on preorded sets, monoids and groups.

In this file we define the filters

• Filter.atTop: corresponds to n → +∞;
• Filter.atBot: corresponds to n → -∞.

Then we prove many lemmas like “if f → +∞, then f ± c → +∞”.

def Filter.atTop {α : Type u_3} [Preorder α] : Filter α

atTop is the filter representing the limit → ∞ on an ordered set. It is generated by the collection of up-sets {b | a ≤ b}. (The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element exists.)

Equations

• Filter.atTop = ⨅ (a : α), Filter.principal (Set.Ici a)

def Filter.atBot {α : Type u_3} [Preorder α] : Filter α

atBot is the filter representing the limit → -∞ on an ordered set. It is generated by the collection of down-sets {b | b ≤ a}. (The preorder need not have a bottom element for this to be well defined, and indeed is trivial when a bottom element exists.)

Equations

• Filter.atBot = ⨅ (a : α), Filter.principal (Set.Iic a)

theorem Filter.mem_atTop {α : Type u_3} [Preorder α] (a : α) : {b : α | a ≤ b} ∈ Filter.atTop

theorem Filter.Ici_mem_atTop {α : Type u_3} [Preorder α] (a : α) : Set.Ici a ∈ Filter.atTop

theorem Filter.Ioi_mem_atTop {α : Type u_3} [Preorder α] [NoMaxOrder α] (x : α) : Set.Ioi x ∈ Filter.atTop

theorem Filter.mem_atBot {α : Type u_3} [Preorder α] (a : α) : {b : α | b ≤ a} ∈ Filter.atBot

theorem Filter.Iic_mem_atBot {α : Type u_3} [Preorder α] (a : α) : Set.Iic a ∈ Filter.atBot

theorem Filter.Iio_mem_atBot {α : Type u_3} [Preorder α] [NoMinOrder α] (x : α) : Set.Iio x ∈ Filter.atBot

theorem Filter.disjoint_atBot_principal_Ioi {α : Type u_3} [Preorder α] (x : α) : Disjoint Filter.atBot (Filter.principal (Set.Ioi x))

theorem Filter.disjoint_atTop_principal_Iio {α : Type u_3} [Preorder α] (x : α) : Disjoint Filter.atTop (Filter.principal (Set.Iio x))

theorem Filter.disjoint_atTop_principal_Iic {α : Type u_3} [Preorder α] [NoMaxOrder α] (x : α) : Disjoint Filter.atTop (Filter.principal (Set.Iic x))

theorem Filter.disjoint_atBot_principal_Ici {α : Type u_3} [Preorder α] [NoMinOrder α] (x : α) : Disjoint Filter.atBot (Filter.principal (Set.Ici x))

theorem Filter.disjoint_pure_atTop {α : Type u_3} [Preorder α] [NoMaxOrder α] (x : α) : Disjoint (pure x) Filter.atTop

theorem Filter.disjoint_pure_atBot {α : Type u_3} [Preorder α] [NoMinOrder α] (x : α) : Disjoint (pure x) Filter.atBot

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

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

theorem Filter.disjoint_atBot_atTop {α : Type u_3} [PartialOrder α] [Nontrivial α] : Disjoint Filter.atBot Filter.atTop

theorem Filter.disjoint_atTop_atBot {α : Type u_3} [PartialOrder α] [Nontrivial α] : Disjoint Filter.atTop Filter.atBot

theorem Filter.hasAntitoneBasis_atTop {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x x_1 : α) => x ≤ x_1] : Filter.HasAntitoneBasis Filter.atTop Set.Ici

theorem Filter.atTop_basis {α : Type u_3} [Nonempty α] [SemilatticeSup α] : Filter.HasBasis Filter.atTop (fun (x : α) => True) Set.Ici

theorem Filter.atTop_eq_generate_Ici {α : Type u_3} [SemilatticeSup α] : Filter.atTop = Filter.generate (Set.range Set.Ici)

theorem Filter.atTop_basis' {α : Type u_3} [SemilatticeSup α] (a : α) : Filter.HasBasis Filter.atTop (fun (x : α) => a ≤ x) Set.Ici

theorem Filter.atBot_basis {α : Type u_3} [Nonempty α] [SemilatticeInf α] : Filter.HasBasis Filter.atBot (fun (x : α) => True) Set.Iic

theorem Filter.atBot_basis' {α : Type u_3} [SemilatticeInf α] (a : α) : Filter.HasBasis Filter.atBot (fun (x : α) => x ≤ a) Set.Iic

theorem Filter.atTop_neBot {α : Type u_3} [Nonempty α] [SemilatticeSup α] : Filter.NeBot Filter.atTop

theorem Filter.atBot_neBot {α : Type u_3} [Nonempty α] [SemilatticeInf α] : Filter.NeBot Filter.atBot

@[simp]

theorem Filter.mem_atTop_sets {α : Type u_3} [Nonempty α] [SemilatticeSup α] {s : Set α} : s ∈ Filter.atTop ↔ ∃ (a : α), ∀ b ≥ a, b ∈ s

@[simp]

theorem Filter.mem_atBot_sets {α : Type u_3} [Nonempty α] [SemilatticeInf α] {s : Set α} : s ∈ Filter.atBot ↔ ∃ (a : α), ∀ b ≤ a, b ∈ s

@[simp]

theorem Filter.eventually_atTop {α : Type u_3} [SemilatticeSup α] [Nonempty α] {p : α → Prop} : (∀ᶠ (x : α) in Filter.atTop, p x) ↔ ∃ (a : α), ∀ b ≥ a, p b

@[simp]

theorem Filter.eventually_atBot {α : Type u_3} [SemilatticeInf α] [Nonempty α] {p : α → Prop} : (∀ᶠ (x : α) in Filter.atBot, p x) ↔ ∃ (a : α), ∀ b ≤ a, p b

theorem Filter.eventually_ge_atTop {α : Type u_3} [Preorder α] (a : α) : ∀ᶠ (x : α) in Filter.atTop, a ≤ x

theorem Filter.eventually_le_atBot {α : Type u_3} [Preorder α] (a : α) : ∀ᶠ (x : α) in Filter.atBot, x ≤ a

theorem Filter.eventually_gt_atTop {α : Type u_3} [Preorder α] [NoMaxOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atTop, a < x

theorem Filter.eventually_ne_atTop {α : Type u_3} [Preorder α] [NoMaxOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atTop, x ≠ a

theorem Filter.Tendsto.eventually_gt_atTop {α : Type u_3} {β : Type u_4} [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.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 : Filter.Tendsto f l Filter.atTop) (c : β) : ∀ᶠ (x : α) in l, c ≤ f x

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

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

theorem Filter.eventually_lt_atBot {α : Type u_3} [Preorder α] [NoMinOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atBot, x < a

theorem Filter.eventually_ne_atBot {α : Type u_3} [Preorder α] [NoMinOrder α] (a : α) : ∀ᶠ (x : α) in Filter.atBot, x ≠ a

theorem Filter.Tendsto.eventually_lt_atBot {α : Type u_3} {β : Type u_4} [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α} (hf : Filter.Tendsto f l Filter.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 : Filter.Tendsto f l Filter.atBot) (c : β) : ∀ᶠ (x : α) in l, f x ≤ c

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

theorem Filter.eventually_forall_ge_atTop {α : Type u_3} [Preorder α] {p : α → Prop} : (∀ᶠ (x : α) in Filter.atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in Filter.atTop, p x

theorem Filter.eventually_forall_le_atBot {α : Type u_3} [Preorder α] {p : α → Prop} : (∀ᶠ (x : α) in Filter.atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in Filter.atBot, p x

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

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

theorem Filter.atTop_basis_Ioi {α : Type u_3} [Nonempty α] [SemilatticeSup α] [NoMaxOrder α] : Filter.HasBasis Filter.atTop (fun (x : α) => True) Set.Ioi

theorem Filter.atTop_basis_Ioi' {α : Type u_3} [SemilatticeSup α] [NoMaxOrder α] (a : α) : Filter.HasBasis Filter.atTop (fun (x : α) => a < x) Set.Ioi

theorem Filter.atTop_countable_basis {α : Type u_3} [Nonempty α] [SemilatticeSup α] [Countable α] : Filter.HasCountableBasis Filter.atTop (fun (x : α) => True) Set.Ici

theorem Filter.atBot_countable_basis {α : Type u_3} [Nonempty α] [SemilatticeInf α] [Countable α] : Filter.HasCountableBasis Filter.atBot (fun (x : α) => True) Set.Iic

instance Filter.atTop.isCountablyGenerated {α : Type u_3} [Preorder α] [Countable α] : Filter.IsCountablyGenerated Filter.atTop

Equations

• (_ : Filter.IsCountablyGenerated Filter.atTop) = (_ : Filter.IsCountablyGenerated (⨅ (i : α), Filter.principal (Set.Ici i)))

instance Filter.atBot.isCountablyGenerated {α : Type u_3} [Preorder α] [Countable α] : Filter.IsCountablyGenerated Filter.atBot

Equations

• (_ : Filter.IsCountablyGenerated Filter.atBot) = (_ : Filter.IsCountablyGenerated (⨅ (i : α), Filter.principal (Set.Iic i)))

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

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

theorem Filter.Subsingleton.atTop_eq (α : Type u_6) [Subsingleton α] [Preorder α] : Filter.atTop = ⊤

theorem Filter.Subsingleton.atBot_eq (α : Type u_6) [Subsingleton α] [Preorder α] : Filter.atBot = ⊤

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

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

theorem Filter.Eventually.exists_forall_of_atTop {α : Type u_3} [SemilatticeSup α] [Nonempty α] {p : α → Prop} (h : ∀ᶠ (x : α) in Filter.atTop, p x) : ∃ (a : α), ∀ b ≥ a, p b

theorem Filter.Eventually.exists_forall_of_atBot {α : Type u_3} [SemilatticeInf α] [Nonempty α] {p : α → Prop} (h : ∀ᶠ (x : α) in Filter.atBot, p x) : ∃ (a : α), ∀ b ≤ a, p b

theorem Filter.exists_eventually_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [Nonempty α] {r : α → β → Prop} : (∃ (b : β), ∀ᶠ (a : α) in Filter.atTop, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atTop, ∃ (b : β), ∀ a ≥ a₀, r a b

theorem Filter.exists_eventually_atBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [Nonempty α] {r : α → β → Prop} : (∃ (b : β), ∀ᶠ (a : α) in Filter.atBot, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atBot, ∃ (b : β), ∀ a ≤ a₀, r a b

theorem Filter.frequently_atTop {α : Type u_3} [SemilatticeSup α] [Nonempty α] {p : α → Prop} : (∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b

theorem Filter.frequently_atBot {α : Type u_3} [SemilatticeInf α] [Nonempty α] {p : α → Prop} : (∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b

theorem Filter.frequently_atTop' {α : Type u_3} [SemilatticeSup α] [Nonempty α] [NoMaxOrder α] {p : α → Prop} : (∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b > a, p b

theorem Filter.frequently_atBot' {α : Type u_3} [SemilatticeInf α] [Nonempty α] [NoMinOrder α] {p : α → Prop} : (∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b < a, p b

theorem Filter.Frequently.forall_exists_of_atTop {α : Type u_3} [SemilatticeSup α] [Nonempty α] {p : α → Prop} (h : ∃ᶠ (x : α) in Filter.atTop, p x) (a : α) : ∃ b ≥ a, p b

theorem Filter.Frequently.forall_exists_of_atBot {α : Type u_3} [SemilatticeInf α] [Nonempty α] {p : α → Prop} (h : ∃ᶠ (x : α) in Filter.atBot, p x) (a : α) : ∃ b ≤ a, p b

theorem Filter.map_atTop_eq {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] {f : α → β} : Filter.map f Filter.atTop = ⨅ (a : α), Filter.principal (f '' {a' : α | a ≤ a'})

theorem Filter.map_atBot_eq {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeInf α] {f : α → β} : Filter.map f Filter.atBot = ⨅ (a : α), Filter.principal (f '' {a' : α | a' ≤ a})

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

theorem Filter.tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {m : α → β} {f : Filter α} : Filter.Tendsto m f Filter.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₁ : Filter.Tendsto f₁ l Filter.atTop) : Filter.Tendsto f₂ l Filter.atTop

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

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

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

theorem Filter.atTop_eq_generate_of_forall_exists_le {α : Type u_3} [LinearOrder α] {s : Set α} (hs : ∀ (x : α), ∃ y ∈ s, x ≤ y) : Filter.atTop = Filter.generate (Set.Ici '' s)

theorem Filter.atTop_eq_generate_of_not_bddAbove {α : Type u_3} [LinearOrder α] {s : Set α} (hs : ¬BddAbove s) : Filter.atTop = Filter.generate (Set.Ici '' s)

@[simp]

theorem OrderIso.comap_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (e : α ≃o β) : Filter.comap (⇑e) Filter.atTop = Filter.atTop

@[simp]

theorem OrderIso.comap_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (e : α ≃o β) : Filter.comap (⇑e) Filter.atBot = Filter.atBot

@[simp]

theorem OrderIso.map_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (e : α ≃o β) : Filter.map (⇑e) Filter.atTop = Filter.atTop

@[simp]

theorem OrderIso.map_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (e : α ≃o β) : Filter.map (⇑e) Filter.atBot = Filter.atBot

theorem OrderIso.tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (e : α ≃o β) : Filter.Tendsto (⇑e) Filter.atTop Filter.atTop

theorem OrderIso.tendsto_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (e : α ≃o β) : Filter.Tendsto (⇑e) Filter.atBot Filter.atBot

@[simp]

theorem OrderIso.tendsto_atTop_iff {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] {l : Filter γ} {f : γ → α} (e : α ≃o β) : Filter.Tendsto (fun (x : γ) => e (f x)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

@[simp]

theorem OrderIso.tendsto_atBot_iff {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] {l : Filter γ} {f : γ → α} (e : α ≃o β) : Filter.Tendsto (fun (x : γ) => e (f x)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot

Sequences

theorem Filter.inf_map_atTop_neBot_iff {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [Nonempty α] {F : Filter β} {u : α → β} : Filter.NeBot (F ⊓ Filter.map u Filter.atTop) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U

theorem Filter.inf_map_atBot_neBot_iff {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [Nonempty α] {F : Filter β} {u : α → β} : Filter.NeBot (F ⊓ Filter.map u Filter.atBot) ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U

theorem Filter.extraction_of_frequently_atTop' {P : ℕ → Prop} (h : ∀ (N : ℕ), ∃ n > N, P n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

theorem Filter.extraction_of_frequently_atTop {P : ℕ → Prop} (h : ∃ᶠ (n : ℕ) in Filter.atTop, P n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

theorem Filter.extraction_of_eventually_atTop {P : ℕ → Prop} (h : ∀ᶠ (n : ℕ) in Filter.atTop, P n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

theorem Filter.extraction_forall_of_frequently {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in Filter.atTop, P n k) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

theorem Filter.extraction_forall_of_eventually {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, P n k) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

theorem Filter.extraction_forall_of_eventually' {P : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃ (N : ℕ), ∀ k ≥ N, P n k) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)

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

theorem Filter.exists_le_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : α → β} (h : Filter.Tendsto u Filter.atTop Filter.atTop) (a : α) (b : β) : ∃ a' ≥ a, b ≤ u a'

theorem Filter.exists_le_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : α → β} (h : Filter.Tendsto u Filter.atTop Filter.atBot) (a : α) (b : β) : ∃ a' ≥ a, u a' ≤ b

theorem Filter.exists_lt_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [Preorder β] [NoMaxOrder β] {u : α → β} (h : Filter.Tendsto u Filter.atTop Filter.atTop) (a : α) (b : β) : ∃ a' ≥ a, b < u a'

theorem Filter.exists_lt_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [Preorder β] [NoMinOrder β] {u : α → β} (h : Filter.Tendsto u Filter.atTop Filter.atBot) (a : α) (b : β) : ∃ a' ≥ a, u a' < b

theorem Filter.high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.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.

theorem Filter.low_scores {β : Type u_4} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.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.

theorem Filter.frequently_high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) : ∃ᶠ (n : ℕ) in Filter.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.

theorem Filter.frequently_low_scores {β : Type u_4} [LinearOrder β] [NoMinOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.atBot) : ∃ᶠ (n : ℕ) in Filter.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.

theorem Filter.strictMono_subseq_of_tendsto_atTop {β : Type u_6} [LinearOrder β] [NoMaxOrder β] {u : ℕ → β} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

theorem Filter.strictMono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ (n : ℕ), n ≤ u n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)

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

theorem Filter.tendsto_atTop_add_nonneg_left' {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : ∀ᶠ (x : α) in l, 0 ≤ f x) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_nonpos_left' {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : ∀ᶠ (x : α) in l, f x ≤ 0) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_nonneg_left {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : ∀ (x : α), 0 ≤ f x) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_nonpos_left {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : ∀ (x : α), f x ≤ 0) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_nonneg_right' {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.Tendsto f l Filter.atTop) (hg : ∀ᶠ (x : α) in l, 0 ≤ g x) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_nonpos_right' {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.Tendsto f l Filter.atBot) (hg : ∀ᶠ (x : α) in l, g x ≤ 0) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_nonneg_right {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.Tendsto f l Filter.atTop) (hg : ∀ (x : α), 0 ≤ g x) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_nonpos_right {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.Tendsto f l Filter.atBot) (hg : ∀ (x : α), g x ≤ 0) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.Tendsto.nsmul_atTop {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} (hf : Filter.Tendsto f l Filter.atTop) {n : ℕ} (hn : 0 < n) : Filter.Tendsto (fun (x : α) => n • f x) l Filter.atTop

theorem Filter.Tendsto.nsmul_atBot {α : Type u_3} {β : Type u_4} [OrderedAddCommMonoid β] {l : Filter α} {f : α → β} (hf : Filter.Tendsto f l Filter.atBot) {n : ℕ} (hn : 0 < n) : Filter.Tendsto (fun (x : α) => n • f x) l Filter.atBot

@[deprecated]

theorem Filter.tendsto_bit0_atTop {β : Type u_4} [OrderedAddCommMonoid β] : Filter.Tendsto bit0 Filter.atTop Filter.atTop

@[deprecated]

theorem Filter.tendsto_bit0_atBot {β : Type u_4} [OrderedAddCommMonoid β] : Filter.Tendsto bit0 Filter.atBot Filter.atBot

theorem Filter.tendsto_atTop_of_add_const_left {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} (C : β) (hf : Filter.Tendsto (fun (x : α) => C + f x) l Filter.atTop) : Filter.Tendsto f l Filter.atTop

theorem Filter.tendsto_atBot_of_add_const_left {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} (C : β) (hf : Filter.Tendsto (fun (x : α) => C + f x) l Filter.atBot) : Filter.Tendsto f l Filter.atBot

theorem Filter.tendsto_atTop_of_add_const_right {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} (C : β) (hf : Filter.Tendsto (fun (x : α) => f x + C) l Filter.atTop) : Filter.Tendsto f l Filter.atTop

theorem Filter.tendsto_atBot_of_add_const_right {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} (C : β) (hf : Filter.Tendsto (fun (x : α) => f x + C) l Filter.atBot) : Filter.Tendsto f l Filter.atBot

theorem Filter.tendsto_atTop_of_add_bdd_above_left' {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, f x ≤ C) (h : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop) : Filter.Tendsto g l Filter.atTop

theorem Filter.tendsto_atBot_of_add_bdd_below_left' {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, C ≤ f x) (h : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot) : Filter.Tendsto g l Filter.atBot

theorem Filter.tendsto_atTop_of_add_bdd_above_left {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ (x : α), f x ≤ C) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop → Filter.Tendsto g l Filter.atTop

theorem Filter.tendsto_atBot_of_add_bdd_below_left {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ (x : α), C ≤ f x) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot → Filter.Tendsto g l Filter.atBot

theorem Filter.tendsto_atTop_of_add_bdd_above_right' {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, g x ≤ C) (h : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop) : Filter.Tendsto f l Filter.atTop

theorem Filter.tendsto_atBot_of_add_bdd_below_right' {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ᶠ (x : α) in l, C ≤ g x) (h : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot) : Filter.Tendsto f l Filter.atBot

theorem Filter.tendsto_atTop_of_add_bdd_above_right {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ (x : α), g x ≤ C) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop → Filter.Tendsto f l Filter.atTop

theorem Filter.tendsto_atBot_of_add_bdd_below_right {α : Type u_3} {β : Type u_4} [OrderedCancelAddCommMonoid β] {l : Filter α} {f : α → β} {g : α → β} (C : β) (hC : ∀ (x : α), C ≤ g x) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot → Filter.Tendsto f l Filter.atBot

theorem Filter.tendsto_atTop_add_left_of_le' {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : ∀ᶠ (x : α) in l, C ≤ f x) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_left_of_ge' {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : ∀ᶠ (x : α) in l, f x ≤ C) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_left_of_le {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : ∀ (x : α), C ≤ f x) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_left_of_ge {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : ∀ (x : α), f x ≤ C) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_right_of_le' {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atTop) (hg : ∀ᶠ (x : α) in l, C ≤ g x) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_right_of_ge' {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atBot) (hg : ∀ᶠ (x : α) in l, g x ≤ C) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_right_of_le {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atTop) (hg : ∀ (x : α), C ≤ g x) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atTop

theorem Filter.tendsto_atBot_add_right_of_ge {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} {g : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atBot) (hg : ∀ (x : α), g x ≤ C) : Filter.Tendsto (fun (x : α) => f x + g x) l Filter.atBot

theorem Filter.tendsto_atTop_add_const_left {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : α) => C + f x) l Filter.atTop

theorem Filter.tendsto_atBot_add_const_left {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : α) => C + f x) l Filter.atBot

theorem Filter.tendsto_atTop_add_const_right {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : α) => f x + C) l Filter.atTop

theorem Filter.tendsto_atBot_add_const_right {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] (l : Filter α) {f : α → β} (C : β) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : α) => f x + C) l Filter.atBot

theorem Filter.map_neg_atBot {β : Type u_4} [OrderedAddCommGroup β] : Filter.map Neg.neg Filter.atBot = Filter.atTop

theorem Filter.map_neg_atTop {β : Type u_4} [OrderedAddCommGroup β] : Filter.map Neg.neg Filter.atTop = Filter.atBot

theorem Filter.comap_neg_atBot {β : Type u_4} [OrderedAddCommGroup β] : Filter.comap Neg.neg Filter.atBot = Filter.atTop

theorem Filter.comap_neg_atTop {β : Type u_4} [OrderedAddCommGroup β] : Filter.comap Neg.neg Filter.atTop = Filter.atBot

theorem Filter.tendsto_neg_atTop_atBot {β : Type u_4} [OrderedAddCommGroup β] : Filter.Tendsto Neg.neg Filter.atTop Filter.atBot

theorem Filter.tendsto_neg_atBot_atTop {β : Type u_4} [OrderedAddCommGroup β] : Filter.Tendsto Neg.neg Filter.atBot Filter.atTop

@[simp]

theorem Filter.tendsto_neg_atTop_iff {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] {l : Filter α} {f : α → β} : Filter.Tendsto (fun (x : α) => -f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot

@[simp]

theorem Filter.tendsto_neg_atBot_iff {α : Type u_3} {β : Type u_4} [OrderedAddCommGroup β] {l : Filter α} {f : α → β} : Filter.Tendsto (fun (x : α) => -f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop

@[deprecated]

theorem Filter.tendsto_bit1_atTop {α : Type u_3} [OrderedSemiring α] : Filter.Tendsto bit1 Filter.atTop Filter.atTop

theorem Filter.Tendsto.atTop_mul_atTop {α : Type u_3} {β : Type u_4} [OrderedSemiring α] {l : Filter β} {f : β → α} {g : β → α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x * g x) l Filter.atTop

theorem Filter.tendsto_mul_self_atTop {α : Type u_3} [OrderedSemiring α] : Filter.Tendsto (fun (x : α) => x * x) Filter.atTop Filter.atTop

theorem Filter.tendsto_pow_atTop {α : Type u_3} [OrderedSemiring α] {n : ℕ} (hn : n ≠ 0) : Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.atTop

The monomial function x^n tends to +∞ at +∞ for any positive natural n. A version for positive real powers exists as tendsto_rpow_atTop.

theorem Filter.zero_pow_eventuallyEq {α : Type u_3} [MonoidWithZero α] : (fun (n : ℕ) => 0 ^ n) =ᶠ[Filter.atTop] fun (x : ℕ) => 0

theorem Filter.Tendsto.atTop_mul_atBot {α : Type u_3} {β : Type u_4} [OrderedRing α] {l : Filter β} {f : β → α} {g : β → α} (hf : Filter.Tendsto f l Filter.atTop) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x * g x) l Filter.atBot

theorem Filter.Tendsto.atBot_mul_atTop {α : Type u_3} {β : Type u_4} [OrderedRing α] {l : Filter β} {f : β → α} {g : β → α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x * g x) l Filter.atBot

theorem Filter.Tendsto.atBot_mul_atBot {α : Type u_3} {β : Type u_4} [OrderedRing α] {l : Filter β} {f : β → α} {g : β → α} (hf : Filter.Tendsto f l Filter.atBot) (hg : Filter.Tendsto g l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x * g x) l Filter.atTop

theorem Filter.tendsto_abs_atTop_atTop {α : Type u_3} [LinearOrderedAddCommGroup α] : Filter.Tendsto abs Filter.atTop Filter.atTop

$\lim_{x\to+\infty}|x|=+\infty$

theorem Filter.tendsto_abs_atBot_atTop {α : Type u_3} [LinearOrderedAddCommGroup α] : Filter.Tendsto abs Filter.atBot Filter.atTop

$\lim_{x\to-\infty}|x|=+\infty$

@[simp]

theorem Filter.comap_abs_atTop {α : Type u_3} [LinearOrderedAddCommGroup α] : Filter.comap abs Filter.atTop = Filter.atBot ⊔ Filter.atTop

theorem Filter.Tendsto.atTop_of_const_mul {α : Type u_3} {β : Type u_4} [LinearOrderedSemiring α] {l : Filter β} {f : β → α} {c : α} (hc : 0 < c) (hf : Filter.Tendsto (fun (x : β) => c * f x) l Filter.atTop) : Filter.Tendsto f l Filter.atTop

theorem Filter.Tendsto.atTop_of_mul_const {α : Type u_3} {β : Type u_4} [LinearOrderedSemiring α] {l : Filter β} {f : β → α} {c : α} (hc : 0 < c) (hf : Filter.Tendsto (fun (x : β) => f x * c) l Filter.atTop) : Filter.Tendsto f l Filter.atTop

@[simp]

theorem Filter.tendsto_pow_atTop_iff {α : Type u_3} [LinearOrderedSemiring α] {n : ℕ} : Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0

theorem Filter.nonneg_of_eventually_pow_nonneg {α : Type u_3} [LinearOrderedRing α] {a : α} (h : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a ^ n) : 0 ≤ a

theorem Filter.not_tendsto_pow_atTop_atBot {α : Type u_3} [LinearOrderedRing α] {n : ℕ} : ¬Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.atBot

Multiplication by constant: iff lemmas

theorem Filter.tendsto_const_mul_atTop_of_pos {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

If r is a positive constant, then λ x, r * f x tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_mul_const_atTop_of_pos {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

If r is a positive constant, then λ x, f x * r tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_div_const_atTop_of_pos {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

If r is a positive constant, then x ↦ f x / r tends to infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_const_mul_atTop_iff_pos {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ 0 < r

If f tends to infinity along a nontrivial filter l, then fun x ↦ r * f x tends to infinity if and only if 0 < r.

theorem Filter.tendsto_mul_const_atTop_iff_pos {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ 0 < r

If f tends to infinity along a nontrivial filter l, then fun x ↦ f x * r tends to infinity if and only if 0 < r.

theorem Filter.tendsto_div_const_atTop_iff_pos {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop ↔ 0 < r

If f tends to infinity along a nontrivial filter l, then x ↦ f x * r tends to infinity if and only if 0 < r.

theorem Filter.Tendsto.const_mul_atTop {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop

If a function tends to infinity along a filter, then this function multiplied by a positive constant (on the left) also tends to infinity. For a version working in ℕ or ℤ, use filter.tendsto.const_mul_atTop' instead.

theorem Filter.Tendsto.atTop_mul_const {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop

If a function tends to infinity along a filter, then this function multiplied by a positive constant (on the right) also tends to infinity. For a version working in ℕ or ℤ, use filter.tendsto.atTop_mul_const' instead.

theorem Filter.Tendsto.atTop_div_const {α : Type u_3} {β : Type u_4} [LinearOrderedSemifield α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x / r) l Filter.atTop

If a function tends to infinity along a filter, then this function divided by a positive constant also tends to infinity.

theorem Filter.tendsto_const_mul_pow_atTop {α : Type u_3} [LinearOrderedSemifield α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : 0 < c) : Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atTop

theorem Filter.tendsto_const_mul_pow_atTop_iff {α : Type u_3} [LinearOrderedSemifield α] {c : α} {n : ℕ} : Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atTop ↔ n ≠ 0 ∧ 0 < c

theorem Filter.tendsto_zpow_atTop_atTop {α : Type u_3} [LinearOrderedSemifield α] {n : ℤ} (hn : 0 < n) : Filter.Tendsto (fun (x : α) => x ^ n) Filter.atTop Filter.atTop

theorem Filter.tendsto_const_mul_atBot_of_pos {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot

If r is a positive constant, then λ x, r * f x tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_mul_const_atBot_of_pos {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot

If r is a positive constant, then λ x, f x * r tends to negative infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_const_mul_atTop_of_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot

If r is a negative constant, then λ x, r * f x tends to infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_mul_const_atTop_of_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atBot

If r is a negative constant, then λ x, f x * r tends to infinity along a filter if and only if f tends to negative infinity along the same filter.

theorem Filter.tendsto_const_mul_atBot_of_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop

If r is a negative constant, then λ x, r * f x tends to negative infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_mul_const_atBot_of_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ Filter.Tendsto f l Filter.atTop

If r is a negative constant, then λ x, f x * r tends to negative infinity along a filter if and only if f tends to infinity along the same filter.

theorem Filter.tendsto_const_mul_atTop_iff {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot

The function λ x, r * f x tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem Filter.tendsto_mul_const_atTop_iff {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ 0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot

The function λ x, f x * r tends to infinity along a nontrivial filter if and only if r > 0 and f tends to infinity or r < 0 and f tends to negative infinity.

theorem Filter.tendsto_const_mul_atBot_iff {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop

The function λ x, r * f x tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem Filter.tendsto_mul_const_atBot_iff {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ 0 < r ∧ Filter.Tendsto f l Filter.atBot ∨ r < 0 ∧ Filter.Tendsto f l Filter.atTop

The function λ x, f x * r tends to negative infinity along a nontrivial filter if and only if r > 0 and f tends to negative infinity or r < 0 and f tends to infinity.

theorem Filter.tendsto_const_mul_atTop_iff_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop ↔ r < 0

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ r * f x tends to infinity if and only if r < 0.

theorem Filter.tendsto_mul_const_atTop_iff_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop ↔ r < 0

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x * r tends to infinity if and only if r < 0.

theorem Filter.tendsto_const_mul_atBot_iff_pos {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ 0 < r

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ r * f x tends to negative infinity if and only if 0 < r.

theorem Filter.tendsto_mul_const_atBot_iff_pos {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ 0 < r

If f tends to negative infinity along a nontrivial filter l, then fun x ↦ f x * r tends to negative infinity if and only if 0 < r.

theorem Filter.tendsto_const_mul_atBot_iff_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot ↔ r < 0

If f tends to infinity along a nontrivial filter l, then fun x ↦ r * f x tends to negative infinity if and only if r < 0.

theorem Filter.tendsto_mul_const_atBot_iff_neg {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} [Filter.NeBot l] (h : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot ↔ r < 0

If f tends to infinity along a nontrivial filter l, then fun x ↦ f x * r tends to negative infinity if and only if r < 0.

theorem Filter.Tendsto.neg_const_mul_atTop {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot

If a function tends to infinity along a filter, then this function multiplied by a negative constant (on the left) tends to negative infinity.

theorem Filter.Tendsto.atTop_mul_neg_const {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot

If a function tends to infinity along a filter, then this function multiplied by a negative constant (on the right) tends to negative infinity.

theorem Filter.Tendsto.const_mul_atBot {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atBot

If a function tends to negative infinity along a filter, then this function multiplied by a positive constant (on the left) also tends to negative infinity.

theorem Filter.Tendsto.atBot_mul_const {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atBot

If a function tends to negative infinity along a filter, then this function multiplied by a positive constant (on the right) also tends to negative infinity.

theorem Filter.Tendsto.atBot_div_const {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x / r) l Filter.atBot

If a function tends to negative infinity along a filter, then this function divided by a positive constant also tends to negative infinity.

theorem Filter.Tendsto.neg_const_mul_atBot {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => r * f x) l Filter.atTop

If a function tends to negative infinity along a filter, then this function multiplied by a negative constant (on the left) tends to positive infinity.

theorem Filter.Tendsto.atBot_mul_neg_const {α : Type u_3} {β : Type u_4} [LinearOrderedField α] {l : Filter β} {f : β → α} {r : α} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) : Filter.Tendsto (fun (x : β) => f x * r) l Filter.atTop

If a function tends to negative infinity along a filter, then this function multiplied by a negative constant (on the right) tends to positive infinity.

theorem Filter.tendsto_neg_const_mul_pow_atTop {α : Type u_3} [LinearOrderedField α] {c : α} {n : ℕ} (hn : n ≠ 0) (hc : c < 0) : Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atBot

theorem Filter.tendsto_const_mul_pow_atBot_iff {α : Type u_3} [LinearOrderedField α] {c : α} {n : ℕ} : Filter.Tendsto (fun (x : α) => c * x ^ n) Filter.atTop Filter.atBot ↔ n ≠ 0 ∧ c < 0

theorem Filter.tendsto_atTop' {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] {f : α → β} {l : Filter β} : Filter.Tendsto f Filter.atTop l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≥ a, f b ∈ s

theorem Filter.tendsto_atBot' {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeInf α] {f : α → β} {l : Filter β} : Filter.Tendsto f Filter.atBot l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≤ a, f b ∈ s

theorem Filter.tendsto_atTop_principal {α : Type u_3} {β : Type u_4} [Nonempty β] [SemilatticeSup β] {f : β → α} {s : Set α} : Filter.Tendsto f Filter.atTop (Filter.principal s) ↔ ∃ (N : β), ∀ n ≥ N, f n ∈ s

theorem Filter.tendsto_atBot_principal {α : Type u_3} {β : Type u_4} [Nonempty β] [SemilatticeInf β] {f : β → α} {s : Set α} : Filter.Tendsto f Filter.atBot (Filter.principal s) ↔ ∃ (N : β), ∀ n ≤ N, f n ∈ s

theorem Filter.tendsto_atTop_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] [Preorder β] {f : α → β} : Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≤ f a

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

theorem Filter.tendsto_atTop_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] [Preorder β] {f : α → β} : Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → f a ≤ b

theorem Filter.tendsto_atBot_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeInf α] [Preorder β] {f : α → β} : Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, b ≤ f a

theorem Filter.tendsto_atBot_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeInf α] [Preorder β] {f : α → β} : Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, f a ≤ b

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) : Filter.Tendsto f Filter.atTop Filter.atTop

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) : Filter.Tendsto f Filter.atBot Filter.atBot

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

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

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 Monotone.tendsto_atTop_atTop_iff {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] [Preorder β] {f : α → β} (hf : Monotone f) : Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a

Alias of Filter.tendsto_atTop_atTop_iff_of_monotone.

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

Alias of Filter.tendsto_atBot_atBot_iff_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) : Filter.comap e Filter.atTop = Filter.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) : Filter.comap e Filter.atBot = Filter.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) : Filter.Tendsto (e ∘ f) l Filter.atTop ↔ Filter.Tendsto f l Filter.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) : Filter.Tendsto (e ∘ f) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot

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

theorem Filter.tendsto_finset_range : Filter.Tendsto Finset.range Filter.atTop Filter.atTop

theorem Filter.atTop_finset_eq_iInf {α : Type u_3} : Filter.atTop = ⨅ (x : α), Filter.principal (Set.Ici {x})

theorem Filter.tendsto_atTop_finset_of_monotone {α : Type u_3} {β : Type u_4} [Preorder β] {f : β → Finset α} (h : Monotone f) (h' : ∀ (x : α), ∃ (n : β), x ∈ f n) : Filter.Tendsto f Filter.atTop Filter.atTop

If f is a monotone sequence of Finsets and each x belongs to one of f n, then Tendsto f atTop atTop.

theorem Monotone.tendsto_atTop_finset {α : Type u_3} {β : Type u_4} [Preorder β] {f : β → Finset α} (h : Monotone f) (h' : ∀ (x : α), ∃ (n : β), x ∈ f n) : Filter.Tendsto f Filter.atTop Filter.atTop

Alias of Filter.tendsto_atTop_finset_of_monotone.

---

If f is a monotone sequence of Finsets and each x belongs to one of f n, then Tendsto f atTop atTop.

theorem Filter.tendsto_finset_image_atTop_atTop {β : Type u_4} {γ : Type u_5} [DecidableEq β] {i : β → γ} {j : γ → β} (h : Function.LeftInverse j i) : Filter.Tendsto (Finset.image j) Filter.atTop Filter.atTop

theorem Filter.tendsto_finset_preimage_atTop_atTop {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) : Filter.Tendsto (fun (s : Finset β) => Finset.preimage s f (_ : Set.InjOn f (f ⁻¹' ↑s))) Filter.atTop Filter.atTop

theorem Filter.prod_atTop_atTop_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] : Filter.atTop ×ˢ Filter.atTop = Filter.atTop

theorem Filter.prod_atBot_atBot_eq {β₁ : Type u_6} {β₂ : Type u_7} [Preorder β₁] [Preorder β₂] : Filter.atBot ×ˢ Filter.atBot = Filter.atBot

theorem Filter.prod_map_atTop_eq {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : Filter.map u₁ Filter.atTop ×ˢ Filter.map u₂ Filter.atTop = Filter.map (Prod.map u₁ u₂) Filter.atTop

theorem Filter.prod_map_atBot_eq {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : Filter.map u₁ Filter.atBot ×ˢ Filter.map u₂ Filter.atBot = Filter.map (Prod.map u₁ u₂) Filter.atBot

theorem Filter.Tendsto.subseq_mem {α : Type u_3} {F : Filter α} {V : ℕ → Set α} (h : ∀ (n : ℕ), V n ∈ F) {u : ℕ → α} (hu : Filter.Tendsto u Filter.atTop F) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), u (φ n) ∈ V n

theorem Filter.tendsto_atBot_diagonal {α : Type u_3} [SemilatticeInf α] : Filter.Tendsto (fun (a : α) => (a, a)) Filter.atBot Filter.atBot

theorem Filter.tendsto_atTop_diagonal {α : Type u_3} [SemilatticeSup α] : Filter.Tendsto (fun (a : α) => (a, a)) Filter.atTop Filter.atTop

theorem Filter.Tendsto.prod_map_prod_atBot {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeInf γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Filter.Tendsto f F Filter.atBot) (hg : Filter.Tendsto g G Filter.atBot) : Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atBot

theorem Filter.Tendsto.prod_map_prod_atTop {α : Type u_3} {β : Type u_4} {γ : Type u_5} [SemilatticeSup γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Filter.Tendsto f F Filter.atTop) (hg : Filter.Tendsto g G Filter.atTop) : Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atTop

theorem Filter.Tendsto.prod_atBot {α : Type u_3} {γ : Type u_5} [SemilatticeInf α] [SemilatticeInf γ] {f : α → γ} {g : α → γ} (hf : Filter.Tendsto f Filter.atBot Filter.atBot) (hg : Filter.Tendsto g Filter.atBot Filter.atBot) : Filter.Tendsto (Prod.map f g) Filter.atBot Filter.atBot

theorem Filter.Tendsto.prod_atTop {α : Type u_3} {γ : Type u_5} [SemilatticeSup α] [SemilatticeSup γ] {f : α → γ} {g : α → γ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) : Filter.Tendsto (Prod.map f g) Filter.atTop Filter.atTop

theorem Filter.eventually_atBot_prod_self {α : Type u_3} [SemilatticeInf α] [Nonempty α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ (a : α), ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)

theorem Filter.eventually_atTop_prod_self {α : Type u_3} [SemilatticeSup α] [Nonempty α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ (a : α), ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)

theorem Filter.eventually_atBot_prod_self' {α : Type u_3} [SemilatticeInf α] [Nonempty α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ (a : α), ∀ k ≤ a, ∀ l ≤ a, p (k, l)

theorem Filter.eventually_atTop_prod_self' {α : Type u_3} [SemilatticeSup α] [Nonempty α] {p : α × α → Prop} : (∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ (a : α), ∀ k ≥ a, ∀ l ≥ a, p (k, l)

theorem Filter.eventually_atTop_curry {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] {p : α × β → Prop} (hp : ∀ᶠ (x : α × β) in Filter.atTop, p x) : ∀ᶠ (k : α) in Filter.atTop, ∀ᶠ (l : β) in Filter.atTop, p (k, l)

theorem Filter.eventually_atBot_curry {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] {p : α × β → Prop} (hp : ∀ᶠ (x : α × β) in Filter.atBot, p x) : ∀ᶠ (k : α) in Filter.atBot, ∀ᶠ (l : β) in Filter.atBot, p (k, l)

theorem Filter.map_atTop_eq_of_gc {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (g : β → α) (b' : β) (hf : Monotone f) (gc : ∀ (a : α), ∀ b ≥ b', f a ≤ b ↔ a ≤ g b) (hgi : ∀ b ≥ b', b ≤ f (g b)) : Filter.map f Filter.atTop = Filter.atTop

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 Filter.map_atBot_eq_of_gc {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (g : β → α) (b' : β) (hf : Monotone f) (gc : ∀ (a : α), ∀ b ≤ b', b ≤ f a ↔ g b ≤ a) (hgi : ∀ b ≤ b', f (g b) ≤ b) : Filter.map f Filter.atBot = Filter.atBot

theorem Filter.map_val_atTop_of_Ici_subset {α : Type u_3} [SemilatticeSup α] {a : α} {s : Set α} (h : Set.Ici a ⊆ s) : Filter.map Subtype.val Filter.atTop = Filter.atTop

@[simp]

theorem Filter.map_val_Ici_atTop {α : Type u_3} [SemilatticeSup α] (a : α) : Filter.map Subtype.val Filter.atTop = Filter.atTop

The image of the filter atTop on Ici a under the coercion equals atTop.

@[simp]

theorem Filter.map_val_Ioi_atTop {α : Type u_3} [SemilatticeSup α] [NoMaxOrder α] (a : α) : Filter.map Subtype.val Filter.atTop = Filter.atTop

The image of the filter atTop on Ioi a under the coercion equals atTop.

theorem Filter.atTop_Ioi_eq {α : Type u_3} [SemilatticeSup α] (a : α) : Filter.atTop = Filter.comap Subtype.val Filter.atTop

The atTop filter for an open interval Ioi a comes from the atTop filter in the ambient order.

theorem Filter.atTop_Ici_eq {α : Type u_3} [SemilatticeSup α] (a : α) : Filter.atTop = Filter.comap Subtype.val Filter.atTop

The atTop filter for an open interval Ici a comes from the atTop filter in the ambient order.

@[simp]

theorem Filter.map_val_Iio_atBot {α : Type u_3} [SemilatticeInf α] [NoMinOrder α] (a : α) : Filter.map Subtype.val Filter.atBot = Filter.atBot

The atBot filter for an open interval Iio a comes from the atBot filter in the ambient order.

theorem Filter.atBot_Iio_eq {α : Type u_3} [SemilatticeInf α] (a : α) : Filter.atBot = Filter.comap Subtype.val Filter.atBot

The atBot filter for an open interval Iio a comes from the atBot filter in the ambient order.

@[simp]

theorem Filter.map_val_Iic_atBot {α : Type u_3} [SemilatticeInf α] (a : α) : Filter.map Subtype.val Filter.atBot = Filter.atBot

The atBot filter for an open interval Iic a comes from the atBot filter in the ambient order.

theorem Filter.atBot_Iic_eq {α : Type u_3} [SemilatticeInf α] (a : α) : Filter.atBot = Filter.comap Subtype.val Filter.atBot

The atBot filter for an open interval Iic a comes from the atBot filter in the ambient order.

theorem Filter.tendsto_Ioi_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] {a : α} {f : β → ↑(Set.Ioi a)} {l : Filter β} : Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atTop

theorem Filter.tendsto_Iio_atBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] {a : α} {f : β → ↑(Set.Iio a)} {l : Filter β} : Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atBot

theorem Filter.tendsto_Ici_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] {a : α} {f : β → ↑(Set.Ici a)} {l : Filter β} : Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atTop

theorem Filter.tendsto_Iic_atBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] {a : α} {f : β → ↑(Set.Iic a)} {l : Filter β} : Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atBot

@[simp]

theorem Filter.tendsto_comp_val_Ioi_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] [NoMaxOrder α] {a : α} {f : α → β} {l : Filter β} : Filter.Tendsto (fun (x : ↑(Set.Ioi a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l

@[simp]

theorem Filter.tendsto_comp_val_Ici_atTop {α : Type u_3} {β : Type u_4} [SemilatticeSup α] {a : α} {f : α → β} {l : Filter β} : Filter.Tendsto (fun (x : ↑(Set.Ici a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l

@[simp]

theorem Filter.tendsto_comp_val_Iio_atBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] [NoMinOrder α] {a : α} {f : α → β} {l : Filter β} : Filter.Tendsto (fun (x : ↑(Set.Iio a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l

@[simp]

theorem Filter.tendsto_comp_val_Iic_atBot {α : Type u_3} {β : Type u_4} [SemilatticeInf α] {a : α} {f : α → β} {l : Filter β} : Filter.Tendsto (fun (x : ↑(Set.Iic a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l

theorem Filter.map_add_atTop_eq_nat (k : ℕ) : Filter.map (fun (a : ℕ) => a + k) Filter.atTop = Filter.atTop

theorem Filter.map_sub_atTop_eq_nat (k : ℕ) : Filter.map (fun (a : ℕ) => a - k) Filter.atTop = Filter.atTop

theorem Filter.tendsto_add_atTop_nat (k : ℕ) : Filter.Tendsto (fun (a : ℕ) => a + k) Filter.atTop Filter.atTop

theorem Filter.tendsto_sub_atTop_nat (k : ℕ) : Filter.Tendsto (fun (a : ℕ) => a - k) Filter.atTop Filter.atTop

theorem Filter.tendsto_add_atTop_iff_nat {α : Type u_3} {f : ℕ → α} {l : Filter α} (k : ℕ) : Filter.Tendsto (fun (n : ℕ) => f (n + k)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l

theorem Filter.map_div_atTop_eq_nat (k : ℕ) (hk : 0 < k) : Filter.map (fun (a : ℕ) => a / k) Filter.atTop = Filter.atTop

theorem Filter.tendsto_atTop_atTop_of_monotone' {ι : Type u_1} {α : Type u_3} [Preorder ι] [LinearOrder α] {u : ι → α} (h : Monotone u) (H : ¬BddAbove (Set.range u)) : Filter.Tendsto u Filter.atTop Filter.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)) : Filter.Tendsto u Filter.atBot Filter.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.unbounded_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] [Preorder β] [NoMaxOrder β] {f : α → β} (h : Filter.Tendsto f Filter.atTop Filter.atTop) : ¬BddAbove (Set.range f)

theorem Filter.unbounded_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeSup α] [Preorder β] [NoMinOrder β] {f : α → β} (h : Filter.Tendsto f Filter.atTop Filter.atBot) : ¬BddBelow (Set.range f)

theorem Filter.unbounded_of_tendsto_atTop' {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeInf α] [Preorder β] [NoMaxOrder β] {f : α → β} (h : Filter.Tendsto f Filter.atBot Filter.atTop) : ¬BddAbove (Set.range f)

theorem Filter.unbounded_of_tendsto_atBot' {α : Type u_3} {β : Type u_4} [Nonempty α] [SemilatticeInf α] [Preorder β] [NoMinOrder β] {f : α → β} (h : Filter.Tendsto f Filter.atBot Filter.atBot) : ¬BddBelow (Set.range f)

theorem Filter.tendsto_atTop_of_monotone_of_filter {ι : Type u_1} {α : Type u_3} [Preorder ι] [Preorder α] {l : Filter ι} {u : ι → α} (h : Monotone u) [Filter.NeBot l] (hu : Filter.Tendsto u l Filter.atTop) : Filter.Tendsto u Filter.atTop Filter.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) [Filter.NeBot l] (hu : Filter.Tendsto u l Filter.atBot) : Filter.Tendsto u Filter.atBot Filter.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 ι'} [Filter.NeBot l] (H : Filter.Tendsto (u ∘ φ) l Filter.atTop) : Filter.Tendsto u Filter.atTop Filter.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 ι'} [Filter.NeBot l] (H : Filter.Tendsto (u ∘ φ) l Filter.atBot) : Filter.Tendsto u Filter.atBot Filter.atBot

abbrev Filter.map_atTop_finset_sum_le_of_sum_eq.match_1 {α : Type u_3} {β : Type u_1} {γ : Type u_2} [AddCommMonoid α] {f : β → α} {g : γ → α} (b : Finset γ) (motive : (∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), b ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b) → Prop) : ∀ (x : ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), b ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b), (∀ (v : Finset β) (hv : ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), b ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b), motive (_ : ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), b ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem Filter.map_atTop_finset_sum_le_of_sum_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid α] {f : β → α} {g : γ → α} (h_eq : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ (Finset.sum u' fun (x : γ) => g x) = Finset.sum v' fun (b : β) => f b) : Filter.map (fun (s : Finset β) => Finset.sum s fun (b : β) => f b) Filter.atTop ≤ Filter.map (fun (s : Finset γ) => Finset.sum s fun (x : γ) => g x) Filter.atTop

Let f and g be two maps to the same commutative additive monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∑ b in s, f b) with atTop.map (fun s ↦ ∑ b in s, g b). This is useful to compare the set of limit points of ∑ b in s, f b as s → atTop with the similar set for g.

theorem Filter.map_atTop_finset_prod_le_of_prod_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid α] {f : β → α} {g : γ → α} (h_eq : ∀ (u : Finset γ), ∃ (v : Finset β), ∀ (v' : Finset β), v ⊆ v' → ∃ (u' : Finset γ), u ⊆ u' ∧ (Finset.prod u' fun (x : γ) => g x) = Finset.prod v' fun (b : β) => f b) : Filter.map (fun (s : Finset β) => Finset.prod s fun (b : β) => f b) Filter.atTop ≤ Filter.map (fun (s : Finset γ) => Finset.prod s fun (x : γ) => g x) Filter.atTop

Let f and g be two maps to the same commutative monoid. This lemma gives a sufficient condition for comparison of the filter atTop.map (fun s ↦ ∏ b in s, f b) with atTop.map (fun s ↦ ∏ b in s, g b). This is useful to compare the set of limit points of Π b in s, f b as s → atTop with the similar set for g.

theorem Filter.HasAntitoneBasis.eventually_subset {ι : Type u_1} {α : Type u_3} [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : Filter.HasAntitoneBasis l s) {t : Set α} (ht : t ∈ l) : ∀ᶠ (i : ι) in Filter.atTop, s i ⊆ t

theorem Filter.HasAntitoneBasis.tendsto {ι : Type u_1} {α : Type u_3} [Preorder ι] {l : Filter α} {s : ι → Set α} (hl : Filter.HasAntitoneBasis l s) {φ : ι → α} (h : ∀ (i : ι), φ i ∈ s i) : Filter.Tendsto φ Filter.atTop l

theorem Filter.HasAntitoneBasis.comp_mono {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [SemilatticeSup ι] [Nonempty ι] [Preorder ι'] {l : Filter α} {s : ι' → Set α} (hs : Filter.HasAntitoneBasis l s) {φ : ι → ι'} (φ_mono : Monotone φ) (hφ : Filter.Tendsto φ Filter.atTop Filter.atTop) : Filter.HasAntitoneBasis l (s ∘ φ)

theorem Filter.HasAntitoneBasis.comp_strictMono {α : Type u_3} {l : Filter α} {s : ℕ → Set α} (hs : Filter.HasAntitoneBasis l s) {φ : ℕ → ℕ} (hφ : StrictMono φ) : Filter.HasAntitoneBasis l (s ∘ φ)

theorem Filter.HasAntitoneBasis.subbasis_with_rel {α : Type u_3} {f : Filter α} {s : ℕ → Set α} (hs : Filter.HasAntitoneBasis f s) {r : ℕ → ℕ → Prop} (hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ ⦃m n : ℕ⦄, m < n → r (φ m) (φ n)) ∧ Filter.HasAntitoneBasis f (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".

theorem Filter.exists_seq_tendsto {α : Type u_3} (f : Filter α) [Filter.IsCountablyGenerated f] [Filter.NeBot f] : ∃ (x : ℕ → α), Filter.Tendsto x Filter.atTop f

If f is a nontrivial countably generated filter, then there exists a sequence that converges to f.

theorem Filter.exists_seq_monotone_tendsto_atTop_atTop (α : Type u_6) [SemilatticeSup α] [Nonempty α] [Filter.IsCountablyGenerated Filter.atTop] : ∃ (xs : ℕ → α), Monotone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atTop

theorem Filter.exists_seq_antitone_tendsto_atTop_atBot (α : Type u_6) [SemilatticeInf α] [Nonempty α] [h2 : Filter.IsCountablyGenerated Filter.atBot] : ∃ (xs : ℕ → α), Antitone xs ∧ Filter.Tendsto xs Filter.atTop Filter.atBot

theorem Filter.tendsto_iff_seq_tendsto {α : Type u_3} {β : Type u_4} {f : α → β} {k : Filter α} {l : Filter β} [Filter.IsCountablyGenerated k] : Filter.Tendsto f k l ↔ ∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l

An abstract version of continuity of sequentially continuous functions on metric spaces: if a filter k is countably generated then Tendsto f k l iff for every sequence u converging to k, f ∘ u tends to l.

theorem Filter.tendsto_of_seq_tendsto {α : Type u_3} {β : Type u_4} {f : α → β} {k : Filter α} {l : Filter β} [Filter.IsCountablyGenerated k] : (∀ (x : ℕ → α), Filter.Tendsto x Filter.atTop k → Filter.Tendsto (f ∘ x) Filter.atTop l) → Filter.Tendsto f k l

theorem Filter.eventually_iff_seq_eventually {ι : Type u_6} {l : Filter ι} {p : ι → Prop} [Filter.IsCountablyGenerated l] : (∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Filter.Tendsto x Filter.atTop l → ∀ᶠ (n : ℕ) in Filter.atTop, p (x n)

theorem Filter.frequently_iff_seq_frequently {ι : Type u_6} {l : Filter ι} {p : ι → Prop} [Filter.IsCountablyGenerated l] : (∃ᶠ (n : ι) in l, p n) ↔ ∃ (x : ℕ → ι), Filter.Tendsto x Filter.atTop l ∧ ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)

theorem Filter.subseq_forall_of_frequently {ι : Type u_6} {x : ℕ → ι} {p : ι → Prop} {l : Filter ι} (h_tendsto : Filter.Tendsto x Filter.atTop l) (h : ∃ᶠ (n : ℕ) in Filter.atTop, p (x n)) : ∃ (ns : ℕ → ℕ), Filter.Tendsto (fun (n : ℕ) => x (ns n)) Filter.atTop l ∧ ∀ (n : ℕ), p (x (ns n))

theorem Filter.exists_seq_forall_of_frequently {ι : Type u_6} {l : Filter ι} {p : ι → Prop} [Filter.IsCountablyGenerated l] (h : ∃ᶠ (n : ι) in l, p n) : ∃ (ns : ℕ → ι), Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)

theorem Filter.frequently_iff_seq_forall {ι : Type u_6} {l : Filter ι} {p : ι → Prop} [Filter.IsCountablyGenerated l] : (∃ᶠ (n : ι) in l, p n) ↔ ∃ (ns : ℕ → ι), Filter.Tendsto ns Filter.atTop l ∧ ∀ (n : ℕ), p (ns n)

theorem Filter.tendsto_of_subseq_tendsto {α : Type u_6} {ι : Type u_7} {x : ι → α} {f : Filter α} {l : Filter ι} [Filter.IsCountablyGenerated l] (hxy : ∀ (ns : ℕ → ι), Filter.Tendsto ns Filter.atTop l → ∃ (ms : ℕ → ℕ), Filter.Tendsto (fun (n : ℕ) => x (ns (ms n))) Filter.atTop f) : Filter.Tendsto x l f

A sequence converges if every subsequence has a convergent subsequence.

theorem Filter.subseq_tendsto_of_neBot {α : Type u_3} {f : Filter α} [Filter.IsCountablyGenerated f] {u : ℕ → α} (hx : Filter.NeBot (f ⊓ Filter.map u Filter.atTop)) : ∃ (θ : ℕ → ℕ), StrictMono θ ∧ Filter.Tendsto (u ∘ θ) Filter.atTop f

theorem exists_lt_mul_self {R : Type u_6} [LinearOrderedSemiring R] (a : R) : ∃ x ≥ 0, a < x * x

theorem exists_le_mul_self {R : Type u_6} [LinearOrderedSemiring R] (a : R) : ∃ x ≥ 0, a ≤ x * x

theorem Monotone.piecewise_eventually_eq_iUnion {ι : Type u_1} {α : Type u_3} {β : α → Type u_6} [Preorder ι] {s : ι → Set α} [(i : ι) → DecidablePred fun (x : α) => x ∈ s i] [DecidablePred fun (x : α) => x ∈ ⋃ (i : ι), s i] (hs : Monotone s) (f : (a : α) → β a) (g : (a : α) → β a) (a : α) : ∀ᶠ (i : ι) in Filter.atTop, Set.piecewise (s i) f g a = Set.piecewise (⋃ (i : ι), s i) f g a

theorem Antitone.piecewise_eventually_eq_iInter {ι : Type u_1} {α : Type u_3} {β : α → Type u_6} [Preorder ι] {s : ι → Set α} [(i : ι) → DecidablePred fun (x : α) => x ∈ s i] [DecidablePred fun (x : α) => x ∈ ⋂ (i : ι), s i] (hs : Antitone s) (f : (a : α) → β a) (g : (a : α) → β a) (a : α) : ∀ᶠ (i : ι) in Filter.atTop, Set.piecewise (s i) f g a = Set.piecewise (⋂ (i : ι), s i) f g a

theorem Function.Injective.map_atTop_finset_sum_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid α] {g : γ → β} (hg : Function.Injective g) {f : β → α} (hf : ∀ x ∉ Set.range g, f x = 0) : Filter.map (fun (s : Finset γ) => Finset.sum s fun (i : γ) => f (g i)) Filter.atTop = Filter.map (fun (s : Finset β) => Finset.sum s fun (i : β) => f i) Filter.atTop

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to an additive commutative monoid. Suppose that f x = 0 outside of the range of g. Then the filters atTop.map (fun s ↦ ∑ i in s, f (g i)) and atTop.map (fun s ↦ ∑ i in s, f i) coincide.

This lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.

theorem Function.Injective.map_atTop_finset_prod_eq {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid α] {g : γ → β} (hg : Function.Injective g) {f : β → α} (hf : ∀ x ∉ Set.range g, f x = 1) : Filter.map (fun (s : Finset γ) => Finset.prod s fun (i : γ) => f (g i)) Filter.atTop = Filter.map (fun (s : Finset β) => Finset.prod s fun (i : β) => f i) Filter.atTop

Let g : γ → β be an injective function and f : β → α be a function from the codomain of g to a commutative monoid. Suppose that f x = 1 outside of the range of g. Then the filters atTop.map (fun s ↦ ∏ i in s, f (g i)) and atTop.map (fun s ↦ ∏ i in s, f i) coincide.

The additive version of this lemma is used to prove the equality ∑' x, f (g x) = ∑' y, f y under the same assumptions.