instOrderBotSubtypeIsIdempotentElem

Mathlib.Algebra.Order.Ring.Idempotent

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

English

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

Русский

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

LaTeX

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

Lean4

instance {M₀ : Type*} [CommMonoidWithZero M₀] : OrderBot { a : M₀ // IsIdempotentElem a }
    where
  bot := ⟨0, .zero⟩
  bot_le _ := zero_mul _

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

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

Разделы

Аффилиация

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