copy — Mathlib

English

Copy of a nonunital star subalgebra with a new carrier is equal to the original if the carrier is equal.

Русский

Копия ненулевой звёздной подалгебры с новым носителем равна исходной, если носитель равен исходному.

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 : NonUnitalStarSubalgebra R A) (s : Set A) (hs : s = ↑S) : NonUnitalStarSubalgebra R A :=
  { S.toNonUnitalSubalgebra.copy s hs with
    star_mem' :=
      @fun x (hx : x ∈ s) => by
        change star x ∈ s
        rw [hs] at hx ⊢
        exact S.star_mem' hx }

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