le_maximum_of_length_pos_iff

Mathlib.Data.List.MinMax

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

English

For nonempty l and any b, b ≤ maximum_of_length_pos(l) iff b ≤ maximum(l).

Русский

При непустом l и любом b верно: b ≤ maximum_of_length_pos(l) эквивалентно b ≤ maximum(l).

LaTeX

$$$b \\le \\text{maximum\\_of\\_length\\_pos}(l) \\iff b \\le \\max(l)$$$

Lean4

@[simp]
theorem le_maximum_of_length_pos_iff {b : α} (h : 0 < l.length) : b ≤ maximum_of_length_pos h ↔ b ≤ l.maximum :=
  WithBot.le_unbot_iff _

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

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

Разделы

Аффилиация

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