antitone_vecEmpty — Mathlib

English

Let α be a set with a preorder. The function obtained by prepending a fixed value a to the empty vector, vecCons a vecEmpty, is antitone; i.e., whenever i ≤ j in Fin(1), the value at i is at least the value at j.

Русский

Пусть α упорядочено предельным отношением. Функция, получаемая кононацией значения a в начало пустого вектора vecCons a vecEmpty, является антимонотонной: если i ≤ j в Fin(1), то f(i) ≥ f(j).

LaTeX

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

Lean4

@[simp]
theorem antitone_vecEmpty : Antitone (vecCons a vecEmpty)
  | ⟨0, _⟩, ⟨0, _⟩, _ => le_rfl

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