isChain_raise' — Mathlib

English

For any list l and n, the list raise' l n is a chain with respect to the less-than relation, i.e., strictly increasing.

Русский

Для любой последовательности l и n список raise' l n образует цепочку по отношению меньше, то есть строго возрастающий.

LaTeX

$$$\forall l\,n,\, \text{List.IsChain}(<)(\text{raise'}(l,n))$$$

Lean4

theorem isChain_raise' : ∀ (l) (n), List.IsChain (· < ·) (raise' l n)
  | [], _ => .nil
  | [_], _ => .singleton _
  | _ :: _ :: _, _ => .cons_cons (by omega) (isChain_raise' (_ :: _) _)

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