le_of_lt — Mathlib

English

If a list is sorted by <, then it is sorted by ≤ (in a preorder).

Русский

Если список отсортирован по отношению меньше, то он отсортирован по нестрогому порядку (≤).

LaTeX

$$$\\text{[Preorder } \\alpha]\\; \\{l:\\text{List}(\\alpha)\\}\\ to\\; l.\\text{Sorted}(<) \\Rightarrow l.\\text{Sorted}(\\le)$$$

Lean4

protected theorem le_of_lt [Preorder α] {l : List α} (h : l.Sorted (· < ·)) : l.Sorted (· ≤ ·) :=
  h.imp le_of_lt

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