coe_copy — Mathlib

English

The coercion of a copied substructure equals the original set, i.e., (S.copy s hs : Set R) = s under the appropriate equality hs.

Русский

Приведение копированного подструктурного множества равняется исходному множеству при заданном равенстве.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_copy (S : NonUnitalStarSubsemiring R) (s : Set R) (hs : s = ↑S) : (S.copy s hs : Set R) = s :=
  rfl

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