coe_maximum_of_length_pos

Mathlib.Data.List.MinMax

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

English

For a nonempty list, the value maximum_of_length_pos equals the maximum of the list.

Русский

Для непустого списка maximum_of_length_pos равен максимуму списка.

LaTeX

$$$\\text{maximum\\_of\\_length\\_pos}(l) = \\max(l)$$$

Lean4

@[simp]
theorem coe_maximum_of_length_pos (h : 0 < l.length) : (l.maximum_of_length_pos h : α) = l.maximum :=
  WithBot.coe_unbot _ _

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

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

Разделы

Аффилиация

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