SeparatesPoints — Mathlib

English

A subalgebra of continuous maps separates points if for any distinct points x,y in α there exists f in the subalgebra such that f(x) ≠ f(y).

Русский

Подалгебра непрерывных отображений разделяет точки, если для любых различных x,y в α существует f в подалгебре, такая что f(x) ≠ f(y).

LaTeX

$$$\\text{SeparatesPoints}(s) := \\{\\, \\text{for all } x \\neq y, \\exists f\\in s: f(x) \\neq f(y) \\,\\}.$$$

Lean4

/-- A version of `Set.SeparatesPoints` for subalgebras of the continuous functions,
used for stating the Stone-Weierstrass theorem.
-/
abbrev SeparatesPoints (s : Subalgebra R C(α, A)) : Prop :=
  Set.SeparatesPoints ((fun f : C(α, A) => (f : α → A)) '' (s : Set C(α, A)))

Похожие утверждения