Map and comap of Filter.atTop and Filter.atBot

@[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