raise'_sorted

Mathlib.Logic.Equiv.Finset

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

← MathLib Explorer

English

For any list l and n, the list raise' l n is sorted in increasing order.

Русский

Для любой последовательности l и n список raise' l n упорядочен по возрастанию.

LaTeX

$$$\forall l\,n,\, \text{List.Sorted}(<)(\text{raise'}(l,n))$$$

Lean4

/-- `raise' l n` is a strictly increasing sequence. -/
theorem raise'_sorted (l n) : List.Sorted (· < ·) (raise' l n) :=
  (isChain_raise' _ _).pairwise

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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