CPolynomialAt_congr — Mathlib

English

If an open set s and f,g agree on s, then f is a polynomial on s iff g is a polynomial on s.

Русский

Если открытое множество s и функции f, g совпадают на s, то f является полиномом на s тогда и только тогда, когда g является полиномом на s.

LaTeX

$$$\text{IsOpen } s \land (f =_s g) \Rightarrow (CPolynomialOn 𝕜 f s \iff CPolynomialOn 𝕜 g s).$$$

Lean4

theorem CPolynomialAt_congr (h : f =ᶠ[𝓝 x] g) : CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x :=
  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩

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