minimum_of_length_pos_le_of_mem — Mathlib

English

Let α be a linearly ordered set and l a list with a ∈ l and w with 0 < length(l). Then minimum_of_length_pos w ≤ a.

Русский

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

LaTeX

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

Lean4

theorem minimum_of_length_pos_le_of_mem (h : a ∈ l) (w : 0 < l.length) : l.minimum_of_length_pos w ≤ a :=
  le_maximum_of_length_pos_of_mem (α := αᵒᵈ) h w

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