eqOn_adjoin — Mathlib

English

If D1 and D2 agree on s, they agree on adjoin(R,s).

Русский

Если D1 и D2 совпадают на s, то они совпадают на adjoin(R,s).

LaTeX

$$Set.EqOn (Derivation.instFunLike.coe D1) (Derivation.instFunLike.coe D2) s → Set.EqOn (Derivation.instFunLike.coe D1) (Derivation.instFunLike.coe D2) (Algebra.adjoin R s)$$

Lean4

theorem eqOn_adjoin {s : Set A} (h : Set.EqOn D1 D2 s) : Set.EqOn D1 D2 (adjoin R s) := fun _ hx =>
  Algebra.adjoin_induction (hx := hx) h (fun r => (D1.map_algebraMap r).trans (D2.map_algebraMap r).symm)
    (fun x y _ _ hx hy => by simp only [map_add, *]) fun x y _ _ hx hy => by simp only [leibniz, *]

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