raise_lower' — Mathlib

English

For all l and n, the identity raise' (lower' l n) n = l holds, i.e., the two operations undo each other regardless of l and n.

Русский

Для всех l и n выполняется raise'(lower'(l,n), n) = l; две операции взаимно обратны независимо от l и n.

LaTeX

$$$\forall l\,n, \text{raise'}(\text{lower'}(l,n), n) = l$$$

Lean4

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

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