continuous — Mathlib

English

If a function is polynomial on the whole space (i.e., a CPolynomialOn everywhere), then the function is continuous.

Русский

Если функция является полиномиальной на всем пространстве (то есть $f$ является CPolynomialOn на всюду), то она непрерывна.

LaTeX

$$$CPolynomialOn\\ 𝕜\\ f\\ univ \\rightarrow \\mathrm{Continuous}\\ f$$$

Lean4

/-- Continuously polynomial everywhere implies continuous -/
theorem continuous {f : E → F} (fa : CPolynomialOn 𝕜 f univ) : Continuous f := by rw [← continuousOn_univ];
  exact fa.continuousOn

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