succ_top

Mathlib.Data.List.Intervals

URI: https://scilib.ai/kg/mathlib#List.Ico.succ_top

English

If n ≤ m, then Ico n (m+1) = Ico n m ++ [m].

Русский

Если n ≤ m, то Ico n (m+1) = Ico n m ++ [m].

LaTeX

$$$\forall {n,m:\mathbb{N}},\ (n \le m) \Rightarrow \operatorname{Ico}(n,m+1) = \operatorname{Ico}(n,m)\append [m]$$$

Lean4

theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = Ico n m ++ [m] :=
  by
  rwa [← succ_singleton, append_consecutive]
  exact Nat.le_succ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru