minimum_le_of_mem' — Mathlib

English

Let α be a linearly ordered set. For any nonempty list l of elements of α and any a ∈ l, the minimum of l is at most a.

Русский

Пусть α упорядочено линейно. Для любого непустого списка l элементов α и любого a ∈ l выполняется min(l) ≤ a.

LaTeX

$$$\\forall l\\in\\mathsf{List}(\\alpha)\\,\\forall a\\in l:\\ \\min(l)\\le a$$$

Lean4

theorem minimum_le_of_mem' (ha : a ∈ l) : minimum l ≤ (a : WithTop α) :=
  le_of_not_gt <| not_lt_minimum_of_mem' ha

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