max_idem

Mathlib.Order.MinMax

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

← MathLib Explorer

English

Max is idempotent: for every a, max(a, a) = a.

Русский

Макс идемпотентен: для любого a выполняется max(a, a) = a.

LaTeX

$$$$\max(a,a) = a.$$$$

Lean4

/-- An instance asserting that `max a a = a` -/
instance max_idem : Std.IdempotentOp (α := α) max where
  idempotent := by
    simp
      -- short-circuit type class inference

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

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

Разделы

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

Аффилиация

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