coe_copy — Mathlib

English

Let S be a nonunital subsemiring of R and let s be a subset of R such that s equals the underlying set of S. Then the underlying set of the copied subsemiring S.copy s hs is exactly s; i.e., the copy operation does not change the carrier when the carrier is unchanged.

Русский

Пусть S — подполусемиринг без единицы в R и пусть s — подмножество R, удовлетворяющее равенству s = ↑S. Тогда копия S, ограниченная множеством s и соответствующими доказательствами hs, имеет тот же носитель, что и s; то есть копия не изменяет множество.

LaTeX

$$$ (S.copy s\ \text{hs} : \\ Set\,R) = s$$$

Lean4

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

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