append_consecutive — Mathlib

English

If n ≤ m and m ≤ l, then Ico n m ++ Ico m l = Ico n l.

Русский

Если n ≤ m ≤ l, то Ico n m ++ Ico m l = Ico n l.

LaTeX

$$$\forall {n,m,l:\mathbb{N}},\ Ico(n,m)\ append\ Ico(m,l) = Ico(n,l)$ при условии $n \le m$ и $m \le l$$$

Lean4

theorem append_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) : Ico n m ++ Ico m l = Ico n l :=
  by
  dsimp only [Ico]
  convert range'_append using 2
  · rw [Nat.one_mul, Nat.add_sub_cancel' hnm]
  · cutsat

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