le_maximum_of_length_pos_of_mem — Mathlib

English

Let α be a linearly ordered set and l a list with an element a ∈ l and w such that 0 < length(l). Then a ≤ maximum_of_length_pos w.

Русский

Пусть α — линейно упорядоченное множество, l — список, содержащий элемент a, и существует w, для которого 0 < длина(l). Тогда a ≤ maximum_of_length_pos w.

LaTeX

$$$\\forall {\\alpha} [\\mathrm{LinearOrder}(\\alpha)], \\forall {l : \\mathrm List}(\\alpha), {\\forall a \\in l}, \\forall w : 0 < l.length, a \\le l.maximum_of_length_pos w$$$

Lean4

theorem le_maximum_of_length_pos_of_mem (h : a ∈ l) (w : 0 < l.length) : a ≤ l.maximum_of_length_pos w :=
  by
  simp only [le_maximum_of_length_pos_iff]
  exact le_maximum_of_mem' h

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