canonicallyOrderedAdd

Mathlib.Algebra.Order.PUnit

URI: https://scilib.ai/kg/mathlib#PUnit.canonicallyOrderedAdd

← MathLib Explorer

English

The one-element type PUnit carries a canonical ordered additive structure.

Русский

Единичный тип PUnit несёт канонически упорядоченное сложение.

LaTeX

$$$\\text{CanonicallyOrderedAdd}\\; \\text{PUnit}$$$

Lean4

instance canonicallyOrderedAdd : CanonicallyOrderedAdd PUnit
    where
  exists_add_of_le {_ _} _ := ⟨unit, by subsingleton⟩
  le_add_self _ _ := trivial
  le_self_add _ _ := trivial

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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