instOrderTopSubtypeIsIdempotentElem

Mathlib.Algebra.Order.Ring.Idempotent

URI: https://scilib.ai/kg/mathlib#instOrderTopSubtypeIsIdempotentElem

English

The idempotent-subset E has a top element given by (1,0).

Русский

У множества идемпотентных пар есть верхняя граница, которая задаётся парой (1,0).

LaTeX

$$$top = (1,0) \in E$ and\; a \le top$ for all $a \in E$$$

Lean4

instance {M : Type*} [CommMonoid M] : OrderTop { a : M // IsIdempotentElem a }
    where
  top := ⟨1, .one⟩
  le_top _ := mul_one _

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

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

Разделы

Аффилиация

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