derivation_eqOn_supported — Mathlib

English

If two derivations agree on X_i for all i in a set s, then they agree on all polynomials supported on s.

Русский

Если две производные согласованы на X_i для всех i из множества s, то они согласованы на всех полиномах, поддерживаемых на s.

LaTeX

$$$\\\\forall D_1 D_2, \\\\forall s, \\\\mathrm{Set}.EqOn(D_1 \\circ X, D_2 \\circ X) s \\\\Rightarrow \\\\forall f \\\\in supported(R,s), \\\\ D_1 f = D_2 f$$$

Lean4

/-- If two derivations agree on `X i`, `i ∈ s`, then they agree on all polynomials from
`MvPolynomial.supported R s`. -/
theorem derivation_eqOn_supported {D₁ D₂ : Derivation R (MvPolynomial σ R) A} {s : Set σ}
    (h : Set.EqOn (D₁ ∘ X) (D₂ ∘ X) s) {f : MvPolynomial σ R} (hf : f ∈ supported R s) : D₁ f = D₂ f :=
  Derivation.eqOn_adjoin (Set.forall_mem_image.2 h) hf

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