Documentation

Mathlib.Order.Filter.AtTopBot

Filter.atTop and Filter.atBot filters on preorders, monoids and groups. #

In this file we define the filters

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

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

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
Instances For
    def Filter.atBot {α : Type u_3} [Preorder α] :

    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
    Instances For
      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 β) [l.NeBot] :
      ¬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 β) [l.NeBot] :
      ¬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.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 yp y) ∀ᶠ (x : α) in Filter.atTop, p x
      theorem Filter.eventually_forall_le_atBot {α : Type u_3} [Preorder α] {p : αProp} :
      (∀ᶠ (x : α) in Filter.atBot, yx, p y) ∀ᶠ (x : α) in Filter.atBot, p x
      theorem Filter.Tendsto.eventually_forall_ge_atTop {α : Type u_3} {β : Type u_4} [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 yp y
      theorem Filter.Tendsto.eventually_forall_le_atBot {α : Type u_3} {β : Type u_4} [Preorder β] {l : Filter α} {p : βProp} {f : αβ} (hf : Filter.Tendsto f l Filter.atBot) (h_evtl : ∀ᶠ (x : β) in Filter.atBot, p x) :
      ∀ᶠ (x : α) in l, yf x, p y
      @[instance 200]
      instance Filter.atTop.isCountablyGenerated {α : Type u_3} [Preorder α] [Countable α] :
      Filter.atTop.IsCountablyGenerated
      Equations
      • =
      @[instance 200]
      instance Filter.atBot.isCountablyGenerated {α : Type u_3} [Preorder α] [Countable α] :
      Filter.atBot.IsCountablyGenerated
      Equations
      • =
      instance OrderDual.instIsCountablyGeneratedAtTop {α : Type u_3} [Preorder α] [Filter.atBot.IsCountablyGenerated] :
      Filter.atTop.IsCountablyGenerated
      Equations
      • = inst
      instance OrderDual.instIsCountablyGeneratedAtBot {α : Type u_3} [Preorder α] [Filter.atTop.IsCountablyGenerated] :
      Filter.atBot.IsCountablyGenerated
      Equations
      • = inst
      theorem IsTop.atTop_eq {α : Type u_3} [Preorder α] {a : α} (ha : IsTop a) :
      Filter.atTop = Filter.principal (Set.Ici a)
      theorem IsBot.atBot_eq {α : Type u_3} [Preorder α] {a : α} (ha : IsBot a) :
      Filter.atBot = Filter.principal (Set.Iic a)
      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.atTop_eq_generate_Ici {α : Type u_3} [Preorder α] :
      Filter.atTop = Filter.generate (Set.range Set.Ici)
      theorem Filter.Frequently.forall_exists_of_atTop {α : Type u_3} [Preorder α] {p : αProp} (h : ∃ᶠ (x : α) in Filter.atTop, p x) (a : α) :
      ba, p b
      theorem Filter.Frequently.forall_exists_of_atBot {α : Type u_3} [Preorder α] {p : αProp} (h : ∃ᶠ (x : α) in Filter.atBot, p x) (a : α) :
      ba, p b
      theorem Filter.hasAntitoneBasis_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] :
      Filter.atTop.HasAntitoneBasis Set.Ici
      theorem Filter.atTop_basis {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] :
      Filter.atTop.HasBasis (fun (x : α) => True) Set.Ici
      theorem Filter.atTop_basis_Ioi {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] [NoMaxOrder α] :
      Filter.atTop.HasBasis (fun (x : α) => True) Set.Ioi
      theorem Filter.atTop_basis_Ioi' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [NoMaxOrder α] (a : α) :
      Filter.atTop.HasBasis (fun (x : α) => a < x) Set.Ioi
      theorem Filter.atTop_basis' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (a : α) :
      Filter.atTop.HasBasis (fun (x : α) => a x) Set.Ici
      theorem Filter.atTop_neBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] :
      Filter.atTop.NeBot
      theorem Filter.atTop_neBot_iff {α : Type u_6} [Preorder α] :
      Filter.atTop.NeBot Nonempty α IsDirected α fun (x1 x2 : α) => x1 x2
      theorem Filter.atBot_neBot_iff {α : Type u_6} [Preorder α] :
      Filter.atBot.NeBot Nonempty α IsDirected α fun (x1 x2 : α) => x1 x2
      @[simp]
      theorem Filter.mem_atTop_sets {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] {s : Set α} :
      s Filter.atTop ∃ (a : α), ba, b s
      @[simp]
      theorem Filter.eventually_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] :
      (∀ᶠ (x : α) in Filter.atTop, p x) ∃ (a : α), ba, p b
      theorem Filter.frequently_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] :
      (∃ᶠ (x : α) in Filter.atTop, p x) ∀ (a : α), ba, p b
      theorem Filter.Eventually.exists_forall_of_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] :
      (∀ᶠ (x : α) in Filter.atTop, p x)∃ (a : α), ba, p b

      Alias of the forward direction of Filter.eventually_atTop.

      theorem Filter.exists_eventually_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] {r : αβProp} :
      (∃ (b : β), ∀ᶠ (a : α) in Filter.atTop, r a b) ∀ᶠ (a₀ : α) in Filter.atTop, ∃ (b : β), aa₀, r a b
      theorem Filter.map_atTop_eq {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] {f : αβ} :
      Filter.map f Filter.atTop = ⨅ (a : α), Filter.principal (f '' {a' : α | a a'})
      theorem Filter.frequently_atTop' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] [NoMaxOrder α] :
      (∃ᶠ (x : α) in Filter.atTop, p x) ∀ (a : α), b > a, p b
      theorem Filter.atTop_countable_basis {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] [Countable α] :
      Filter.atTop.HasCountableBasis (fun (x : α) => True) Set.Ici
      theorem Filter.atBot_basis_Iio {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] [NoMinOrder α] :
      Filter.atBot.HasBasis (fun (x : α) => True) Set.Iio
      theorem Filter.atBot_basis_Iio' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [NoMinOrder α] (a : α) :
      Filter.atBot.HasBasis (fun (x : α) => x < a) Set.Iio
      theorem Filter.atBot_basis' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (a : α) :
      Filter.atBot.HasBasis (fun (x : α) => x a) Set.Iic
      theorem Filter.atBot_basis {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] :
      Filter.atBot.HasBasis (fun (x : α) => True) Set.Iic
      theorem Filter.atBot_neBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] :
      Filter.atBot.NeBot
      @[simp]
      theorem Filter.mem_atBot_sets {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] {s : Set α} :
      s Filter.atBot ∃ (a : α), ba, b s
      @[simp]
      theorem Filter.eventually_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] :
      (∀ᶠ (x : α) in Filter.atBot, p x) ∃ (a : α), ba, p b
      theorem Filter.frequently_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] :
      (∃ᶠ (x : α) in Filter.atBot, p x) ∀ (a : α), ba, p b
      theorem Filter.Eventually.exists_forall_of_atBot {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] :
      (∀ᶠ (x : α) in Filter.atBot, p x)∃ (a : α), ba, p b

      Alias of the forward direction of Filter.eventually_atBot.

      theorem Filter.exists_eventually_atBot {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] {r : αβProp} :
      (∃ (b : β), ∀ᶠ (a : α) in Filter.atBot, r a b) ∀ᶠ (a₀ : α) in Filter.atBot, ∃ (b : β), aa₀, r a b
      theorem Filter.map_atBot_eq {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] {f : αβ} :
      Filter.map f Filter.atBot = ⨅ (a : α), Filter.principal (f '' {a' : α | a' a})
      theorem Filter.frequently_atBot' {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : αProp} [Nonempty α] [NoMinOrder α] :
      (∃ᶠ (x : α) in Filter.atBot, p x) ∀ (a : α), b < a, p b
      theorem Filter.atBot_countable_basis {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Nonempty α] [Countable α] :
      Filter.atBot.HasCountableBasis (fun (x : α) => True) Set.Iic
      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.atBotFilter.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.atTopFilter.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.atBotFilter.Tendsto f l Filter.atBot
      theorem Filter.atTop_eq_generate_of_forall_exists_le {α : Type u_3} [LinearOrder α] {s : Set α} (hs : ∀ (x : α), ys, 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.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 : ), kN, 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.inf_map_atTop_neBot_iff {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {F : Filter β} {u : αβ} [Nonempty α] :
      (F Filter.map u Filter.atTop).NeBot UF, ∀ (N : α), nN, u n U
      theorem Filter.exists_le_of_tendsto_atTop {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {u : αβ} [Preorder β] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {u : αβ} [Preorder β] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {u : αβ} [Preorder β] [NoMaxOrder β] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {u : αβ} [Preorder β] [NoMinOrder β] (h : Filter.Tendsto u Filter.atTop Filter.atBot) (a : α) (b : β) :
      a'a, u a' < b
      theorem Filter.inf_map_atBot_neBot_iff {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {F : Filter β} {u : αβ} :
      (F Filter.map u Filter.atBot).NeBot UF, ∀ (N : α), nN, u n U
      theorem Filter.high_scores {β : Type u_4} [LinearOrder β] [NoMaxOrder β] {u : β} (hu : Filter.Tendsto u Filter.atTop Filter.atTop) (N : ) :
      nN, 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 : ) :
      nN, 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_4} [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_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_atTop_atBot_of_antitone {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : αβ} (hf : Antitone f) (h : ∀ (b : β), ∃ (a : α), f a b) :
      Filter.Tendsto f Filter.atTop Filter.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) :
      Filter.Tendsto f Filter.atBot Filter.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) :
      Filter.Tendsto f Filter.atBot Filter.atTop
      theorem Filter.tendsto_atTop' {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} {l : Filter β} :
      Filter.Tendsto f Filter.atTop l sl, ∃ (a : α), ba, f b s
      theorem Filter.tendsto_atTop_principal {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} {s : Set β} :
      Filter.Tendsto f Filter.atTop (Filter.principal s) ∃ (N : α), nN, f n s
      theorem Filter.tendsto_atTop_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] :
      Filter.Tendsto f Filter.atTop Filter.atTop ∀ (b : β), ∃ (i : α), ∀ (a : α), i ab 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 α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] :
      Filter.Tendsto f Filter.atTop Filter.atBot ∀ (b : β), ∃ (i : α), ∀ (a : α), i af a b
      theorem Filter.tendsto_atTop_atTop_iff_of_monotone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] (hf : Monotone f) :
      Filter.Tendsto f Filter.atTop Filter.atTop ∀ (b : β), ∃ (a : α), b f a
      theorem Filter.tendsto_atTop_atBot_iff_of_antitone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] (hf : Antitone f) :
      Filter.Tendsto f Filter.atTop Filter.atBot ∀ (b : β), ∃ (a : α), f a b
      theorem Filter.tendsto_atBot' {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} {l : Filter β} :
      Filter.Tendsto f Filter.atBot l sl, ∃ (a : α), ba, f b s
      theorem Filter.tendsto_atBot_principal {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} {s : Set β} :
      Filter.Tendsto f Filter.atBot (Filter.principal s) ∃ (N : α), nN, f n s
      theorem Filter.tendsto_atBot_atTop {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] :
      Filter.Tendsto f Filter.atBot Filter.atTop ∀ (b : β), ∃ (i : α), ai, b f a
      theorem Filter.tendsto_atBot_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] :
      Filter.Tendsto f Filter.atBot Filter.atBot ∀ (b : β), ∃ (i : α), ai, f a b
      theorem Filter.tendsto_atBot_atBot_iff_of_monotone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] (hf : Monotone f) :
      Filter.Tendsto f Filter.atBot Filter.atBot ∀ (b : β), ∃ (a : α), f a b
      theorem Filter.tendsto_atBot_atTop_iff_of_antitone {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] (hf : Antitone f) :
      Filter.Tendsto f Filter.atBot Filter.atTop ∀ (b : β), ∃ (a : α), b f a
      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 α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] (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 α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {f : αβ} [Preorder β] (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.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 β) => s.preimage f ) Filter.atTop Filter.atTop
      theorem Filter.prod_atTop_atTop_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] :
      Filter.atTop ×ˢ Filter.atTop = Filter.atTop
      instance Filter.instIsCountablyGeneratedAtTopProd {α : Type u_3} {β : Type u_4} [Preorder α] [Filter.atTop.IsCountablyGenerated] [Preorder β] [Filter.atTop.IsCountablyGenerated] :
      Filter.atTop.IsCountablyGenerated
      Equations
      • =
      theorem Filter.tendsto_finset_prod_atTop {ι : Type u_1} {ι' : Type u_2} :
      Filter.Tendsto (fun (p : Finset ι × Finset ι') => p.1 ×ˢ p.2) Filter.atTop Filter.atTop
      theorem Filter.prod_atBot_atBot_eq {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] :
      Filter.atBot ×ˢ Filter.atBot = Filter.atBot
      instance Filter.instIsCountablyGeneratedAtBotProd {α : Type u_3} {β : Type u_4} [Preorder α] [Filter.atBot.IsCountablyGenerated] [Preorder β] [Filter.atBot.IsCountablyGenerated] :
      Filter.atBot.IsCountablyGenerated
      Equations
      • =
      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} [Preorder α] :
      Filter.Tendsto (fun (a : α) => (a, a)) Filter.atBot Filter.atBot
      theorem Filter.tendsto_atTop_diagonal {α : Type u_3} [Preorder α] :
      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} [Preorder γ] {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} [Preorder γ] {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} [Preorder α] [Preorder γ] {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} [Preorder α] [Preorder γ] {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} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : α × αProp} :
      (∀ᶠ (x : α × α) in Filter.atBot, p x) ∃ (a : α), ∀ (k l : α), k al ap (k, l)
      theorem Filter.eventually_atTop_prod_self {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : α × αProp} :
      (∀ᶠ (x : α × α) in Filter.atTop, p x) ∃ (a : α), ∀ (k l : α), a ka lp (k, l)
      theorem Filter.eventually_atBot_prod_self' {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : α × αProp} :
      (∀ᶠ (x : α × α) in Filter.atBot, p x) ∃ (a : α), ka, la, p (k, l)
      theorem Filter.eventually_atTop_prod_self' {α : Type u_3} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {p : α × αProp} :
      (∀ᶠ (x : α × α) in Filter.atTop, p x) ∃ (a : α), ka, la, p (k, l)
      theorem Filter.eventually_atTop_curry {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {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} [Preorder α] [Preorder β] {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_preorder {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 x2] {f : αβ} (hf : Monotone f) (b : β) (hgi : cb, ∃ (x : α), f x = c ∀ (a : α), f a c a x) :
      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_atTop_eq_of_gc {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [PartialOrder β] [IsDirected β fun (x1 x2 : β) => x1 x2] {f : αβ} (g : βα) (b : β) (hf : Monotone f) (gc : ∀ (a : α), cb, f a c a g c) (hgi : cb, c f (g c)) :
      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_preorder {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] [IsDirected β fun (x1 x2 : β) => x1 x2] {f : αβ} (hf : Monotone f) (b : β) (hgi : cb, ∃ (x : α), f x = c ∀ (a : α), c f a x a) :
      Filter.map f Filter.atBot = Filter.atBot
      theorem Filter.map_atBot_eq_of_gc {α : Type u_3} {β : Type u_4} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [PartialOrder β] [IsDirected β fun (x1 x2 : β) => x1 x2] {f : αβ} (g : βα) (b' : β) (hf : Monotone f) (gc : ∀ (a : α), bb', b f a g b a) (hgi : bb', f (g b) b) :
      Filter.map f Filter.atBot = Filter.atBot
      theorem Filter.map_val_atTop_of_Ici_subset {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {a : α} {s : Set α} (h : Set.Ici a s) :
      Filter.map Subtype.val Filter.atTop = Filter.atTop
      @[simp]
      theorem Nat.map_cast_int_atTop :
      Filter.map Nat.cast Filter.atTop = Filter.atTop
      @[simp]
      theorem Filter.map_val_Ici_atTop {α : Type u_3} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] (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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [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} [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] {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 α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} [NoMaxOrder β] (h : Filter.Tendsto f Filter.atTop Filter.atTop) :
      theorem Filter.unbounded_of_tendsto_atBot {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} [NoMinOrder β] (h : Filter.Tendsto f Filter.atTop Filter.atBot) :
      theorem Filter.unbounded_of_tendsto_atTop' {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} [NoMaxOrder β] (h : Filter.Tendsto f Filter.atBot Filter.atTop) :
      theorem Filter.unbounded_of_tendsto_atBot' {α : Type u_3} {β : Type u_4} [Nonempty α] [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Preorder β] {f : αβ} [NoMinOrder β] (h : Filter.Tendsto f Filter.atBot Filter.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 : 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) [l.NeBot] (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 ι'} [l.NeBot] (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 ι'} [l.NeBot] (H : Filter.Tendsto (u φ) l Filter.atBot) :
      Filter.Tendsto u Filter.atBot Filter.atBot
      theorem Filter.HasAntitoneBasis.eventually_subset {ι : Type u_1} {α : Type u_3} [Preorder ι] {l : Filter α} {s : ιSet α} (hl : l.HasAntitoneBasis 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 : l.HasAntitoneBasis 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} [Nonempty ι] [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] [Preorder ι'] {l : Filter α} {s : ι'Set α} (hs : l.HasAntitoneBasis s) {φ : ιι'} (φ_mono : Monotone φ) (hφ : Filter.Tendsto φ Filter.atTop Filter.atTop) :
      l.HasAntitoneBasis (s φ)
      theorem Filter.HasAntitoneBasis.comp_strictMono {α : Type u_3} {l : Filter α} {s : Set α} (hs : l.HasAntitoneBasis s) {φ : } (hφ : StrictMono φ) :
      l.HasAntitoneBasis (s φ)
      theorem Filter.HasAntitoneBasis.subbasis_with_rel {α : Type u_3} {f : Filter α} {s : Set α} (hs : f.HasAntitoneBasis s) {r : Prop} (hr : ∀ (m : ), ∀ᶠ (n : ) in Filter.atTop, r m n) :
      ∃ (φ : ), StrictMono φ (∀ ⦃m n : ⦄, m < nr (φ m) (φ n)) f.HasAntitoneBasis (s φ)

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

      theorem Filter.exists_seq_tendsto {α : Type u_3} (f : Filter α) [f.IsCountablyGenerated] [f.NeBot] :
      ∃ (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) [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Filter.atTop.IsCountablyGenerated] :
      ∃ (xs : α), Monotone xs Filter.Tendsto xs Filter.atTop Filter.atTop
      theorem Filter.exists_seq_antitone_tendsto_atTop_atBot (α : Type u_6) [Preorder α] [Nonempty α] [IsDirected α fun (x1 x2 : α) => x1 x2] [Filter.atBot.IsCountablyGenerated] :
      ∃ (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 β} [k.IsCountablyGenerated] :
      Filter.Tendsto f k l ∀ (x : α), Filter.Tendsto x Filter.atTop kFilter.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 β} [k.IsCountablyGenerated] :
      (∀ (x : α), Filter.Tendsto x Filter.atTop kFilter.Tendsto (f x) Filter.atTop l)Filter.Tendsto f k l
      theorem Filter.eventually_iff_seq_eventually {ι : Type u_6} {l : Filter ι} {p : ιProp} [l.IsCountablyGenerated] :
      (∀ᶠ (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} [l.IsCountablyGenerated] :
      (∃ᶠ (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} [l.IsCountablyGenerated] (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} [l.IsCountablyGenerated] :
      (∃ᶠ (n : ι) in l, p n) ∃ (ns : ι), Filter.Tendsto ns Filter.atTop l ∀ (n : ), p (ns n)
      theorem Filter.tendsto_of_subseq_tendsto {α : Type u_3} {ι : Type u_6} {x : ια} {f : Filter α} {l : Filter ι} [l.IsCountablyGenerated] (hxy : ∀ (ns : ι), Filter.Tendsto ns Filter.atTop l∃ (ms : ), Filter.Tendsto (fun (n : ) => x (ns (ms n))) Filter.atTop f) :

      A sequence converges if every subsequence has a convergent subsequence.

      theorem Filter.subseq_tendsto_of_neBot {α : Type u_3} {f : Filter α} [f.IsCountablyGenerated] {u : α} (hx : (f Filter.map u Filter.atTop).NeBot) :
      ∃ (θ : ), StrictMono θ Filter.Tendsto (u θ) Filter.atTop f
      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, (s i).piecewise f g a = (⋃ (i : ι), s i).piecewise 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, (s i).piecewise f g a = (⋂ (i : ι), s i).piecewise f g a
      theorem Nat.eventually_pow_lt_factorial_sub (c : ) (d : ) :
      ∀ᶠ (n : ) in Filter.atTop, c ^ n < (n - d).factorial
      theorem Nat.eventually_mul_pow_lt_factorial_sub (a : ) (c : ) (d : ) :
      ∀ᶠ (n : ) in Filter.atTop, a * c ^ n < (n - d).factorial
      @[deprecated Nat.eventually_pow_lt_factorial_sub]
      theorem Nat.exists_pow_lt_factorial (c : ) :
      n0 > 1, nn0, c ^ n < (n - 1).factorial
      @[deprecated Nat.eventually_mul_pow_lt_factorial_sub]
      theorem Nat.exists_mul_pow_lt_factorial (a : ) (c : ) :
      ∃ (n0 : ), nn0, a * c ^ n < (n - 1).factorial