isChain_cons_raise'

Mathlib.Logic.Equiv.Finset

URI: https://scilib.ai/kg/mathlib#Denumerable.isChain_cons_raise'

English

For any list l and m, List.IsChain(<) (m :: raise' l (m+1)) holds.

Русский

Для любой последовательности l и числа m выполняется, что список (m :: raise' l (m+1)) образует цепочку.

LaTeX

$$$\forall l\,m,\, \text{List.IsChain}(<)(m :: \text{raise'}(l,(m+1)))$$$

Lean4

theorem isChain_cons_raise' (l m) : List.IsChain (· < ·) (m :: raise' l (m + 1)) :=
  isChain_raise' (m :: l) 0

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

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

Разделы

Аффилиация

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