copy_eq — Mathlib

English

If you copy a subalgebra along with a carrier that is equal to the original, you recover the original subalgebra.

Русский

Если скопировать подалгебру вместе с носителем, равным исходному, получается та же подалгебра.

LaTeX

$$$ S^{\mathrm{copy}} = S $ whenever the new carrier equals the original.$$

Lean4

theorem copy_eq (S : Subalgebra R A) (s : Set A) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

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