English
Under the same HasBasis hypothesis and with a chosen point x_i in s_i when p_i holds, eventual constancy of f is equivalent to f being constant on s_i for some i with p_i.
Русский
При тех же предположениях о базисе и выборе x_i ∈ s_i при p_i, равенство требует: существует i с p_i, и для всех y ∈ s_i, f y равно f(x_i).
LaTeX
$$$\\\\forall h \\\\text{HasBasis } p s, \\\\forall x_i \\\\in s_i \\\\;(p i \Rightarrow x_i \\\\in s_i) \\\\Rightarrow \\\\Big( \\\\text{EventuallyConst } f l \\\\Leftrightarrow \\\\exists i, p i \\\\wedge \\\\forall y \\\\in s_i, \\\\; f y = f(x_i) \Big)$$$
Lean4
theorem eventuallyConst_iff {ι : Sort*} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) :
EventuallyConst f l ↔ ∃ i, p i ∧ ∀ x ∈ s i, ∀ y ∈ s i, f x = f y :=
(h.map f).subsingleton_iff.trans <| by simp only [Set.Subsingleton, forall_mem_image]
