not_maximum_lt_of_mem' — Mathlib

English

For any a ∈ l, the maximum l is not strictly less than a (in WithBot ordering).

Русский

Для любого a ∈ l максимум списка не меньше a; в частности, не меньше и не строго больше.

LaTeX

$$$\forall ha.\; ha \in l \rightarrow \Not (\operatorname{maximum} l < (a : \mathrm{WithBot}\; \alpha))$$$

Lean4

theorem not_maximum_lt_of_mem' (ha : a ∈ l) : ¬maximum l < (a : WithBot α) := by
  cases h : l.maximum <;> simp_all [not_maximum_lt_of_mem ha]

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