ofDigits_monotone — Mathlib

English

If p ≤ q and L is a digit list, then ofDigits p L ≤ ofDigits q L.

Русский

Если p ≤ q и L — список цифр, то ofDigits p L ≤ ofDigits q L.

LaTeX

$$$ \forall p,q\ L:\; L \text{ is a List Nat},\; p \le q \Rightarrow \mathrm{ofDigits}(p,L) \le \mathrm{ofDigits}(q,L) $$$

Lean4

@[mono]
theorem ofDigits_monotone {p q : ℕ} (L : List ℕ) (h : p ≤ q) : ofDigits p L ≤ ofDigits q L := by
  induction L with
  | nil => rfl
  | cons _ _ hi =>
    simp only [ofDigits, cast_id, add_le_add_iff_left]
    exact Nat.mul_le_mul h hi

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