min_idem

Mathlib.Order.MinMax

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

← MathLib Explorer

English

Min is idempotent: for every a, min(a, a) = a.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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