coe_top

Mathlib.Algebra.Group.Subsemigroup.Defs

URI: https://scilib.ai/kg/mathlib#Subsemigroup.coe_top

English

The carrier of the top subsemigroup is the whole set M.

Русский

Носитель верхней подполугруппы равен всему множеству M.

LaTeX

$$$ ((\\top : Subsemigroup M) : Set M) = \\mathsf{Set.univ} $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru