English
If f tends to a limit different from f(x) along a nontrivial filter l2, then f cannot be continuous at x provided the limit along l1 is l2 and l1 refines nhds x.
Русский
Если f стремится к пределу, отличному от f(x), вдоль нетривиального фильтра, то при условии, что предел вдоль l1 равен l2 и l1 ≤ 𝓝 x, функция не непрерывна в x.
LaTeX
$$$\\mathrm{Tendsto}(f, l_1, l_2) \\;[l_1\\neq\\bot] \\;\\land\\; l_1 \\le 𝓝(x) \\land \\mathrm{Disjoint}(𝓝(f(x)), l_2) \\Rightarrow \\neg\\mathrm{ContinuousAt}(f, x)$$$
Lean4
/-- If a function `f` tends to somewhere other than `𝓝 (f x)` at `x`,
then `f` is not continuous at `x`
-/
theorem not_continuousAt_of_tendsto {f : X → Y} {l₁ : Filter X} {l₂ : Filter Y} {x : X} (hf : Tendsto f l₁ l₂)
[l₁.NeBot] (hl₁ : l₁ ≤ 𝓝 x) (hl₂ : Disjoint (𝓝 (f x)) l₂) : ¬ContinuousAt f x := fun cont ↦
(cont.mono_left hl₁).not_tendsto hl₂ hf
