ext_of_adjoin_eq_top — Mathlib

English

If the adjoin of a set is the whole algebra, two derivations equal on the set are equal overall.

Русский

Если адъюнкт множества даёт всю алгебру, две производные равны на множестве, значит равны во всей алгебре.

LaTeX

$$ext_of_adjoin_eq_top (s : Set A) (hs : adjoin R s = ⊤) (h : Set.EqOn D1 D2 s) : D1 = D2$$

Lean4

/-- If adjoin of a set is the whole algebra, then any two derivations equal on this set are equal
on the whole algebra. -/
theorem ext_of_adjoin_eq_top (s : Set A) (hs : adjoin R s = ⊤) (h : Set.EqOn D1 D2 s) : D1 = D2 :=
  ext fun _ => eqOn_adjoin h <| hs.symm ▸ trivial

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