English
If l has a basis given by p i and sets s i, then the function f is eventually constant along l iff there exists an i with p i and f is constant on s i.
Русский
Если фильтр имеет базис, задаваемый p i и множества s i, то функция f становится константной вдоль этого базиса тогда и только тогда, когда существует некоторый i с p i, и f постоянна на каждом s i.
LaTeX
$$$\\\\forall p,s,f\\\\; (l.HasBasis p s) \\\\Rightarrow \\\\Big(\\\\text{EventuallyConst } f l \\\\Leftrightarrow \\\\exists i, p i \\\\wedge \\\\forall x\\\\in s i, \\\\forall y\\\\in s i, f x = f y\\\\Big)$$$
Lean4
/-- The proposition that a function is eventually constant along a filter on the domain. -/
def EventuallyConst (f : α → β) (l : Filter α) : Prop :=
(map f l).Subsingleton
