rel_head!_of_mem — Mathlib

English

If i is a member of the sorted list l.val, then i ≤ l.val.head! (head of the list).

Русский

Если i принадлежит отсортированному списку l.val, то i ≤ head(l.val).

LaTeX

$$$$ \\text{If } i \\in l.\\text{val}, \\quad i \\le l.\\text{val.head!}. $$$$

Lean4

theorem rel_head!_of_mem [Inhabited I] {i : I} {l : Products I} (hi : i ∈ l.val) : i ≤ l.val.head! :=
  List.Sorted.le_head! (List.isChain_iff_pairwise.mp l.prop) hi

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