gt_of_ge — Mathlib

English

If a list is sorted by ≥ and is nodup, then it is sorted by > (strict).

Русский

Если список отсортирован по ≥ и не содержит повторов, то он отсортирован по >.

LaTeX

$$$ h: l.\\text{Sorted}(\\ge) \\land l.\\text{Nodup} \Rightarrow l.\\text{Sorted}(>) $$$

Lean4

protected theorem gt_of_ge [PartialOrder α] {l : List α} (h₁ : l.Sorted (· ≥ ·)) (h₂ : l.Nodup) : l.Sorted (· > ·) :=
  h₁.imp₂ (fun _ _ => lt_of_le_of_ne) <| by simp_rw [ne_comm]; exact h₂

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