coe_le_maximum_iff

Mathlib.Data.List.MinMax

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

English

For any a, a ≤ maximum(l) holds if and only if there exists b ∈ l with a ≤ b.

Русский

Для любого a выполнено a ≤ максимум(l) тогда и только если существует b ∈ l с a ≤ b.

LaTeX

$$$a \\le \\max(l) \\iff \\exists b \\in l:\\ a \\le b$$$

Lean4

theorem coe_le_maximum_iff : a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b := by induction l <;> simp [maximum_cons, *]

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

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

Разделы

Аффилиация

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