SeparatesPoints — Mathlib

English

A family A of functions from α to β is said to separate points if for any distinct x,y ∈ α there exists f ∈ A with f(x) ≠ f(y).

Русский

Множество функций A из α в β разделяет точки, если для любых разных x,y ∈ α существует функция f ∈ A с f(x) ≠ f(y).

LaTeX

$$SeparatesPoints(A) := ∀ {x y : α}, x ≠ y → ∃ f ∈ A, f(x) ≠ f(y)$$

Lean4

/-- A set of functions "separates points"
if for each pair of distinct points there is a function taking different values on them. -/
def SeparatesPoints {α β : Type*} (A : Set (α → β)) : Prop :=
  ∀ ⦃x y : α⦄, x ≠ y → ∃ f ∈ A, (f x : β) ≠ f y

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