evalEval_surjective — Mathlib

English

The map evalEval x y is surjective: for every r ∈ R there exists a polynomial whose evaluation at (x,y) is r.

Русский

Отображение evalEval x y сюръективно: для каждого r ∈ R существует полином, для которого его значение в (x,y) равно r, например CC r.

LaTeX

$$$ \\forall r \\in R, \\exists p \\in R[X][Y], p.evalEval\\ x\\ y = r $$$

Lean4

theorem evalEval_surjective (x y : R) : Function.Surjective <| evalEval x y := fun y => ⟨CC y, evalEval_CC ..⟩

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