eq_cons

Mathlib.Data.List.Intervals

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

English

If n < m then Ico n m = n :: Ico (n+1) m.

Русский

Если n < m, то Ico n m = n :: Ico (n+1) m.

LaTeX

$$$\forall {n,m}:\ instLTNat.lt n m \Rightarrow \operatorname{Ico}(n,m) = n $::\operatorname{Ico}(n+1,m)$$$$

Lean4

theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = n :: Ico (n + 1) m :=
  by
  rw [← append_consecutive (Nat.le_succ n) h, succ_singleton]
  rfl

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

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

Разделы

Аффилиация

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