copy_eq — Mathlib

English

Equality of copies corresponds to equality of carriers; i.e., if hs holds, then the copies coincide with the original.

Русский

Равенство копий соответствует равенству носителей; если hs выполняется, копии совпадают с исходным.

LaTeX

$$copy_eq_2 (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S$$

Lean4

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

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