copy — Mathlib

English

Copy creates a new StarSubsemiring with the same carrier; the copy operation preserves the carrier.

Русский

Copy создаёт новую StarSubsemiring с тем же носителем; копирование сохраняет носитель.

LaTeX

$$$ S.copy\; s\; hs = S $$$

Lean4

/-- Copy of a non-unital star subalgebra with a new `carrier` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (S : StarSubsemiring R) (s : Set R) (hs : s = ↑S) : StarSubsemiring R
    where
  toSubsemiring := Subsemiring.copy S.toSubsemiring s hs
  star_mem' := @fun a ha => hs ▸ (S.star_mem' (by simpa [hs] using ha) : star a ∈ (S : Set R))

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