minimum_of_length_pos_mem — Mathlib

English

Let α be a linearly ordered set and l a finite nonempty list of α. Then the element produced by minimum_of_length_pos with a proof that l is nonempty lies in l.

Русский

Пусть α — линейно упорядоченное множество, а l — конечный непустой список элементов α. Тогда элемент minimum_of_length_pos, получаемый из доказательства того, что длина l положительна, принадлежит списку l.

LaTeX

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

Lean4

theorem minimum_of_length_pos_mem (h : 0 < l.length) : minimum_of_length_pos h ∈ l :=
  maximum_of_length_pos_mem (α := αᵒᵈ) h

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