maximum_ne_bot_of_length_pos

Mathlib.Data.List.MinMax

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

English

If the length of l is positive, then l.maximum ≠ ⊥.

Русский

Если длина списка положительна, то максимум списка не равен ⊥.

LaTeX

$$$0 < |l| \\Rightarrow \\max(l) \\neq \\bot$$$

Lean4

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

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

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

Разделы

Аффилиация

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