raise_sorted

Mathlib.Logic.Equiv.Multiset

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

English

For all l and n, raise l n is nondecreasing.

Русский

Для всех l и n, raise l n неубывает.

LaTeX

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

Lean4

/-- `raise l n` is a non-decreasing sequence. -/
theorem raise_sorted (l n) : List.Sorted (· ≤ ·) (raise l n) :=
  (isChain_raise _ _).pairwise

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

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

Разделы

Аффилиация

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