le_cons — Mathlib

English

A pointwise order comparison of q with cons x p is equivalent to comparing the head and the tail: q ≤ cons x p iff q(0) ≤ x and tail q ≤ p.

Русский

Похождение лексического порядка: q ≤ cons x p эквивалентно q(0) ≤ x и tail q ≤ p.

LaTeX

$$$q \\le \\mathrm{cons}(x,p) \\iff q(0) \\le x \\land \\mathrm{tail}(q) \\le p$$$

Lean4

theorem le_cons [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} :
    q ≤ cons x p ↔ q 0 ≤ x ∧ tail q ≤ p :=
  forall_fin_succ.trans <| and_congr Iff.rfl <| forall_congr' fun j ↦ by simp [tail]

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