coe_top — Mathlib

English

In any multiplicative monoid M, the top submonoid has as its underlying set the whole set M; i.e., the submonoid that contains every element of M corresponds to all of M as a set.

Русский

В любой моноиде с умножением M верхний субмонод содержит все элементы M; то есть подмножество, состоящее из всех элементов, совпадает с M как множеством.

LaTeX

$$$((\top : \mathrm{Submonoid} M) : \mathrm{Set} M) = \mathrm{Set.univ}$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_top : ((⊤ : Submonoid M) : Set M) = Set.univ :=
  rfl

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