Definition of Filter.atTop and Filter.atBot filters

In this file we define the filters

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

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} ∈ atTop

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

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

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

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

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

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

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

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

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

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

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

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.atTop_eq_generate_Ici {α : Type u_3} [Preorder α] : atTop = generate (Set.range Set.Ici)

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

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

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

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

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 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 g : (a : α) → β a) (a : α) : ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋂ (i : ι), s i).piecewise f g a