coe_set_mk — Mathlib

English

Let G be a group and S a submonoid of G for which inverses of its elements stay in S. Then the underlying set of the subgroup constructed from S equals S.

Русский

Пусть G — группа, S — подмономоид G, удовлетворяющий свойству, что обратные элементы S остаются в S. Тогда носитель подгруппы, построенной из S, равен S.

LaTeX

$$$\\operatorname{carrier}(\\mathrm{mk}(S,h)) = S$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_set_mk {s : Submonoid G} (h_inv) : (mk s h_inv : Set G) = s :=
  rfl

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