sorted_lt_range' — Mathlib

English

For all a,b ∈ Nat and s ≠ 0, List.range' a b s is sorted with respect to <.

Русский

Для всех a, b ∈ Натуральные и s ≠ 0 список range' a b s упорядочен по <.

LaTeX

$$$$ \forall a,b:\\mathbb{N},\ \forall s:\mathbb{N},\ s \neq 0 \Rightarrow List.Sorted(\lt)(List.range' a b s). $$$$

Lean4

theorem sorted_lt_range' (a b) {s} (hs : s ≠ 0) : Sorted (· < ·) (range' a b s) := by
  induction b generalizing a with
  | zero => simp
  | succ n ih =>
    rw [List.range'_succ]
    refine List.sorted_cons.mpr ⟨fun b hb ↦ ?_, @ih (a + s)⟩
    exact lt_of_lt_of_le (Nat.lt_add_of_pos_right (Nat.zero_lt_of_ne_zero hs)) (List.left_le_of_mem_range' hb)

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