English
Let R be a ring, s a subset of R, and sm, sa be substructures whose underlying sets equal s (with witnesses hm, ha). Then the subring constructed from s, sm, sa is exactly s; i.e., for every x in R, x ∈ Subring.mk' s sm sa hm ha if and only if x ∈ s.
Русский
Пусть R — кольцо, s — подмножество R, и sm, sa — подмонойд и аддитивная подгруппа, чьи множества совпадают с s (с доказательствами hm, ha). Тогда подкольцо Subring.mk' s sm sa hm ha имеет множество элементов, равное s; то есть для каждого x ∈ R выполняется x ∈ Subring.mk' s sm sa hm ha тогда и только тогда, когда x ∈ s.
LaTeX
$$$$ x \in \mathrm{Subring.mk'}(s, sm, sa, hm, ha) \;\Longleftrightarrow\; x \in s $$$$
Lean4
@[simp]
theorem mem_mk' {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R} (ha : ↑sa = s) {x : R} :
x ∈ Subring.mk' s sm sa hm ha ↔ x ∈ s :=
Iff.rfl
