maximum_ne_bot_of_ne_nil

Mathlib.Data.List.MinMax

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

English

If l is nonempty, then its maximum is not bottom (i.e., maximum(l) ≠ ⊥).

Русский

Если список непустой, то его максимум не является нулем снизу (не равен ⊥).

LaTeX

$$$l \\neq \\emptyset \\Rightarrow \\max(l) \\neq \\bot$$$

Lean4

theorem maximum_ne_bot_of_ne_nil (h : l ≠ []) : l.maximum ≠ ⊥ :=
  match l, h with
  | _ :: _, _ => by simp [maximum_cons]

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

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

Разделы

Аффилиация

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