copy_eq — Mathlib

English

Let S be a nonunital subsemiring of R and let s be a subset of R with s equal to the underlying set of S. Then the copy of S built from s is exactly S; i.e., S.copy s = S when hs expresses s is the carrier of S.

Русский

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

LaTeX

$$$S.copy\ s\ hs = S$, где $hs : s = \uparrow S$.$$

Lean4

theorem copy_eq (S : NonUnitalSubsemiring R) (s : Set R) (hs : s = ↑S) : S.copy s hs = S :=
  SetLike.coe_injective hs

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