CPolynomialOn_congr' — Mathlib

English

If f and g are eventually equal on nhds-set s, then CPolynomialOn 𝕜 f s is equivalent to CPolynomialOn 𝕜 g s.

Русский

Если f и g равны почти всюду на nhds-set s, то CPolynomialOn 𝕜 f s эквивалентно CPolynomialOn 𝕜 g s.

LaTeX

$$$ (nhdsSet s).EventuallyEq f g \Rightarrow (CPolynomialOn 𝕜 f s \iff CPolynomialOn 𝕜 g s).$$$

Lean4

theorem CPolynomialOn_congr' {s : Set E} (h : f =ᶠ[𝓝ˢ s] g) : CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s :=
  ⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩

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