English
A set of continuous maps s ⊆ C(α,𝕜) separates points strongly if for every v: α→𝕜 and x,y ∈ α there exists f ∈ s with f(x)=v(x) and f(y)=v(y).
Русский
Множество непрерывных отображений s ⊆ C(α,𝕜) сильносепарирует точки, если для каждого v: α→𝕜 и точек x,y∈α существует f ∈ s, такое что f(x)=v(x) и f(y)=v(y).
LaTeX
$$$\\text{SeparatesPointsStrongly}(s) :\\; \\forall v: α→𝕜, \\forall x,y: α, \\exists f\\in s, f(x)=v(x) \\wedge f(y)=v(y).$$$
Lean4
/-- A set of continuous maps "separates points strongly"
if for each pair of distinct points there is a function with specified values on them.
We give a slightly unusual formulation, where the specified values are given by some
function `v`, and we ask `f x = v x ∧ f y = v y`. This avoids needing a hypothesis `x ≠ y`.
In fact, this definition would work perfectly well for a set of non-continuous functions,
but as the only current use case is in the Stone-Weierstrass theorem,
writing it this way avoids having to deal with casts inside the set.
(This may need to change if we do Stone-Weierstrass on non-compact spaces,
where the functions would be continuous functions vanishing at infinity.)
-/
def SeparatesPointsStrongly (s : Set C(α, 𝕜)) : Prop :=
∀ (v : α → 𝕜) (x y : α), ∃ f ∈ s, (f x : 𝕜) = v x ∧ f y = v y
