maximum_eq_bot

Mathlib.Data.List.MinMax

URI: https://scilib.ai/kg/mathlib#List.maximum_eq_bot

English

The maximum equals bottom exactly when the list is empty.

Русский

Максимум равен нулю тогда, когда список пуст.

LaTeX

$$$\operatorname{maximum} l = \bot \\Leftrightarrow l = []$$

Lean4

@[simp]
theorem maximum_eq_bot {l : List α} : l.maximum = ⊥ ↔ l = [] :=
  argmax_eq_none

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

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

Разделы

Аффилиация

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