surjective_toFn — Mathlib

English

toFn is surjective for all n; i.e., it covers all coefficient vectors.

Русский

toFn сюръективен для всех n; каждый вектор коэффициентов достигается как коэффициенты некоторого многочлена.

LaTeX

$$$\forall n,\; \operatorname{Surjective}(\operatorname{toFn}(n)).$$$

Lean4

theorem surjective_toFn (n : ℕ) : Function.Surjective (toFn (R := R) n) :=
  open Classical in Function.RightInverse.surjective <| toFn_comp_ofFn_eq_id n

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