strictMono_vecEmpty

Mathlib.Order.Fin.Tuple

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

English

The singleton vector cannot be strictly monotone.

Русский

Единственный вектор не может быть строго монотонным.

LaTeX

$$$\text{StrictMono}(![a]) \text{ is false }$.$$

Lean4

@[simp]
theorem strictMono_vecEmpty : StrictMono ![a]
  | ⟨0, _⟩, ⟨0, _⟩, h => (irrefl _ h).elim

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

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

Разделы

Аффилиация

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