copy — Mathlib

English

If s = ↑S, then S.copy s hs = S.

Русский

Если s = ↑S, то S.copy s hs = S.

LaTeX

$$$S.copy\, s\, hs = S\quad\text{ when } hs : s = \uparrow S$$$

Lean4

/-- Copy of a star subalgebra with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy (S : StarSubalgebra R A) (s : Set A) (hs : s = ↑S) : StarSubalgebra R A
    where
  toSubalgebra := Subalgebra.copy S.toSubalgebra s hs
  star_mem' {a} ha := hs ▸ S.star_mem' (by simpa [hs] using ha)

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