card_uIcc — Mathlib

English

For integers a,b, the inclusive interval uIcc(a,b) has length |b−a|+1, so its cardinality is |b−a|+1.

Русский

Для целых a,b любая добавленная длина uIcc(a,b) равна |b−a|+1; кардинал равен |b−a|+1.

LaTeX

$$$|uIcc(a,b)| = |a - b| + 1$$$

Lean4

@[simp]
theorem card_uIcc : #(uIcc a b) = (b - a).natAbs + 1 :=
  (card_map _).trans <|
    (Nat.cast_inj (R := ℤ)).mp <| by
      rw [card_range, Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.natCast_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]

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