sorted_le_replicate

Mathlib.Data.List.Sort

URI: https://scilib.ai/kg/mathlib#List.sorted_le_replicate

English

In any preorder, the list replicate n a is sorted with respect to ≤.

Русский

Во всяком предпорядке список, состоящий из n копий a, упорядочен по ≤.

LaTeX

$$$$ \forall n:\\mathbb{N},\ a:\alpha,\ List.Sorted(\le)(\operatorname{replicate} n\ a). $$$$

Lean4

theorem sorted_le_replicate (n : ℕ) (a : α) [Preorder α] : Sorted (· ≤ ·) (replicate n a) := by simp [sorted_replicate]

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

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

Разделы

Аффилиация

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