cons_le_cons — Mathlib

English

If l' ≤ l in the list order, then a :: l' ≤ a :: l for any a, i.e. prefixing the same element preserves order.

Русский

Если l' ≤ l в списковом порядке, то a :: l' ≤ a :: l для любого a; префиксирование одинакового элемента сохраняет порядок.

LaTeX

$$$l' \\le l \\Rightarrow a \\\\colon l' \\le a \\\\colon l.$$$

Lean4

theorem cons_le_cons [LinearOrder α] (a : α) {l l' : List α} (h : l' ≤ l) : a :: l' ≤ a :: l :=
  by
  rw [le_iff_lt_or_eq] at h ⊢
  exact h.imp .cons (congr_arg _)

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