strictAnti_vecEmpty — Mathlib

English

Let α be a preorder and a fixed a. The function vecCons a vecEmpty is strictly antitone; there are no distinct indices i < j in Fin(1) to witness a violation, so the strictness holds vacuously.

Русский

Пусть α упорядочено, а фиксировано a. Функция vecCons a vecEmpty строго антитонична; поскольку в Fin(1) нет пар i < j, нарушающих условие, строгая антитоничность выполняется вакуумно.

LaTeX

$$$\operatorname{StrictAnti}(\mathrm{vecCons}(a, \mathrm{vecEmpty}))$$$

Lean4

@[simp]
theorem strictAnti_vecEmpty : StrictAnti (vecCons a vecEmpty)
  | ⟨0, _⟩, ⟨0, _⟩, h => (irrefl _ h).elim

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