monotone_vecEmpty

Mathlib.Order.Fin.Tuple

URI: https://scilib.ai/kg/mathlib#monotone_vecEmpty

English

The one-element vector is trivially monotone.

Русский

Вектор из одного элемента тривиально монотонен.

LaTeX

$$$\text{Monotone}(![a]).$$$

Lean4

@[simp]
theorem monotone_vecEmpty : Monotone ![a]
  | ⟨0, _⟩, ⟨0, _⟩, _ => le_refl _

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

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

Разделы

Аффилиация

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