Theorems · Theorem · general topology

Filter.tendsto_atBot_principal

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

Defined in

Mathlib.Order.Filter.AtTopBot.Basic

Cited by

1 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonemptyPreorderIsCodirectedOrder