isChain_raise — Mathlib

English

For every list l and natural n, raise l n is a chain with respect to ≤.

Русский

Для каждого списка l и натурального n, raise l n образует последовательность в порядке ≤.

LaTeX

$$$\\forall l\\,\\forall n,\\ \\text{List.IsChain}(≤)(\\operatorname{raise}(l,n)).$$$

Lean4

theorem isChain_raise : ∀ l n, List.IsChain (· ≤ ·) (raise l n)
  | [], _ => .nil
  | [_], _ => .singleton _
  | _ :: _ :: _, _ => .cons_cons (Nat.le_add_left _ _) (isChain_raise (_ :: _) _)

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