raise_lower — Mathlib

English

If l is sorted in nondecreasing order, then raise (lower l n) n = l.

Русский

Если l неубывающий, то raise (lower l n) n = l.

LaTeX

$$$\\forall \\{l\\}\\,(n),\\ List.Sorted(≤)(n::l) \\Rightarrow \\operatorname{raise}(\\operatorname{lower}(l,n),n) = l.$$$

Lean4

theorem raise_lower : ∀ {l n}, List.Sorted (· ≤ ·) (n :: l) → raise (lower l n) n = l
  | [], _, _ => rfl
  | m :: l, n, h => by
    have : n ≤ m := List.rel_of_sorted_cons h _ List.mem_cons_self
    simp [raise, lower, Nat.sub_add_cancel this, raise_lower h.of_cons]

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