CPolynomialOn_congr — Mathlib

English

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

Русский

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

LaTeX

$$IsOpen s → s.EqOn f g → (CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s)$$

Lean4

theorem CPolynomialOn_congr {s : Set E} (hs : IsOpen s) (h : s.EqOn f g) : CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s :=
  ⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩

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