castLE_natCast — Mathlib

English

If a ≤ n and b ≤ n, then (a : Fin (n+1)) ≤ b.

Русский

Если a ≤ n и b ≤ n, то (a : Fin (n+1)) ≤ b.

LaTeX

$$$\\forall {n,a,b} \\in \\mathbb{N}, b \\le n \\to a \\le b \\to (a : \\mathrm{Fin}(n+1)) \\le b$$$

Lean4

@[simp]
theorem castLE_natCast {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ℕ) :
    letI : NeZero n := ⟨Nat.pos_iff_ne_zero.mp (lt_of_lt_of_le m.pos_of_neZero h)⟩
    Fin.castLE h (a.cast : Fin m) = (a % m : ℕ) :=
  by
  ext
  simp only [coe_castLE, val_natCast]
  rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]

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