head_lt — Mathlib

English

If a is the head of an m-admissible list a :: L, then a is strictly less than every element of L.

Русский

Если a является первым элементом m-допустимого списка a :: L, то a строго меньше каждого элемента L.

LaTeX

$$$\\\\text{If } (a, L) \\,\\text{is the head of an }m\\text{-admissible list, then } a < x \\\\forall x \in L.$$$

Lean4

/-- If `(a :: l)` is `m`-admissible then a is less than all elements of `l` -/
theorem head_lt (a : ℕ) (L : List ℕ) (hl : IsAdmissible m (a :: L)) : ∀ a' ∈ L, a < a' := fun i hi ↦
  (List.sorted_cons.mp hl.sorted).left i hi

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