polynomialFunctions_separatesPoints

English

The family of polynomial functions on X separates points: for any distinct x,y ∈ X there exists a polynomial function f ∈ polynomialFunctions X with f(x) ≠ f(y). A canonical witness is f = X.

Русский

Семейство полином-функций на X разделяет точки: для любых разных x,y ∈ X существует полином-функция f ∈ polynomialFunctions X такая, что f(x) ≠ f(y). В качестве явного примера берём f = X.

LaTeX

$$$\\forall x,y\\in X,\\ x\\neq y\\;\\exists f\\in polynomialFunctions(X)\\text{ s.t. } f(x)\\neq f(y).$$$

Lean4

theorem polynomialFunctions_separatesPoints (X : Set R) : (polynomialFunctions X).SeparatesPoints := fun x y h => by
  -- We use `Polynomial.X`, then clean up.

  refine ⟨_, ⟨⟨_, ⟨⟨Polynomial.X, ⟨Algebra.mem_top, rfl⟩⟩, rfl⟩⟩, ?_⟩⟩
  dsimp; simp only [Polynomial.eval_X]
  exact fun h' => h (Subtype.ext h')

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