English
If a function f tends to b1 along a nontrivial filter a, and b1 and b2 are disjoint, then f cannot tend to b2 along a.
Русский
Если f сходится к b1 по не-тривиальному фильтру a и b1, b2 не пересекаются, то невозможно, чтобы f сходился к b2 по a.
LaTeX
$$$ \\operatorname{Tendsto} f a b_1 \\Rightarrow \\big( \\mathrm{Disjoint}(b_1,b_2) \\Rightarrow \\lnot \\operatorname{Tendsto} f a b_2 \\big) $$$
Lean4
/-- If two filters are disjoint, then a function cannot tend to both of them along a non-trivial
filter. -/
theorem not_tendsto {f : α → β} {a : Filter α} {b₁ b₂ : Filter β} (hf : Tendsto f a b₁) [NeBot a]
(hb : Disjoint b₁ b₂) : ¬Tendsto f a b₂ := fun hf' => (tendsto_inf.2 ⟨hf, hf'⟩).neBot.ne hb.eq_bot
