Theorems · Theorem · general topology

Filter.Tendsto.not_tendsto

∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b₁ b₂ : Filter β},
  Filter.Tendsto f a b₁ → ∀ [a.NeBot], Disjoint b₁ b₂ → ¬Filter.Tendsto f a b₂

If two filters are disjoint, then a function cannot tend to both of them along a non-trivial filter.

Defined in

Mathlib.Order.Filter.Tendsto

Cited by

14 results in Mathlib

Foundations

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

Assumes

Filter.NeBot