isChain_cons_raise

Mathlib.Logic.Equiv.Multiset

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

English

For all l and n, the list n :: raise l n is a chain with respect to ≤.

Русский

Для всех l и n, список n :: raise l n образует цепочку по ≤.

LaTeX

$$$\\forall l\\,\\forall n,\\ \\text{List.IsChain}(≤)(\\text{List.cons } n (\\operatorname{raise}(l,n))).$$$

Lean4

theorem isChain_cons_raise (l n) : List.IsChain (· ≤ ·) (n :: raise l n) :=
  isChain_raise (n :: l) 0

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

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

Разделы

Аффилиация

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