congr — Mathlib

English

If s is open 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 congr {s : Set E} (hs : IsOpen s) (hf : CPolynomialOn 𝕜 f s) (hg : s.EqOn f g) : CPolynomialOn 𝕜 g s :=
  hf.congr' <| mem_nhdsSet_iff_forall.mpr (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)

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