minimum_ne_top_of_ne_nil

Mathlib.Data.List.MinMax

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

English

If l is nonempty, then its minimum is not top (i.e., minimum(l) ≠ top).

Русский

Если список непустой, то его минимум не равен верхнему элементу (не равен top).

LaTeX

$$$l \\neq \\emptyset \\Rightarrow \\min(l) \\neq \\top$$$

Lean4

theorem minimum_ne_top_of_ne_nil (h : l ≠ []) : l.minimum ≠ ⊤ :=
  @maximum_ne_bot_of_ne_nil αᵒᵈ _ _ h

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

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

Разделы

Аффилиация

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