sorted_le_range' — Mathlib

English

For all a,b,s, the list range' a b s is sorted with respect to ≤.

Русский

Для любых a,b,s список range' a b s упорядочен по ≤.

LaTeX

$$$$ \forall a,b,s,\ List.Sorted(\le)(List.range' a b s). $$$$

Lean4

theorem sorted_le_range' (a b s) : Sorted (· ≤ ·) (range' a b s) :=
  by
  by_cases hs : s ≠ 0
  · exact (sorted_lt_range' a b hs).le_of_lt
  · rw [ne_eq, Decidable.not_not] at hs
    simpa [hs] using sorted_le_replicate b a

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