English
Limits are unique up to separability: if f: Y → X tends to a and to b along a nonempty l, then a and b are inseparable.
Русский
Пределы уникальны в смысле разделяемости: если f: Y → X стремится к a и к b вдоль непустой фильтра l, то a и b несопоставимы (inseparable).
LaTeX
$$$\\forall f:Y\\to X,\\ l:\\mathsf{Filter} Y,\\ a,b:X\\; [(l.NeBot)],\\; Tendsto f\\ l (\\mathcal{N} a) \\to Tendsto f\\ l (\\mathcal{N} b) \\Rightarrow Inseparable a b.$$$
Lean4
/-- Limits are unique up to separability.
A weaker version of `tendsto_nhds_unique` for `R1Space`. -/
theorem tendsto_nhds_unique_inseparable {f : Y → X} {l : Filter Y} {a b : X} [NeBot l] (ha : Tendsto f l (𝓝 a))
(hb : Tendsto f l (𝓝 b)) : Inseparable a b :=
.of_nhds_neBot <| neBot_of_le <| le_inf ha hb
