Theorems · Theorem · general topology

Filter.Tendsto.eventually_ne_atTop

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

Defined in

Mathlib.Order.Filter.AtTopBot.Tendsto

Cited by

9 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Quot.sound

Assumes

PreorderNoTopOrder