lt_of_le — Mathlib

English

If a list is sorted by ≤ and the list is nodup, then it is sorted by <.

Русский

Если список отсортирован по ≤ и не содержит дубликатов, то он отсортирован по <.

LaTeX

$$$ h_1: l.\\text{Sorted}(\\le) \\to h_2: l.\\text{Nodup} \\Rightarrow l.\\text{Sorted}(<) $$$

Lean4

protected theorem lt_of_le [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≤ ·)) (h₂ : l.Nodup) : l.Sorted (· < ·) :=
  h₁.imp₂ (fun _ _ => lt_of_le_of_ne) h₂

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