card_uIcc — Mathlib

English

For any a,b ∈ Fin n, the number of elements in the unsigned interval uIcc(a,b) equals (b − a) in Z, natAbs, plus 1.

Русский

Для любых a,b ∈ Fin n число элементов в неотрицательном интервале uIcc(a,b) равно |b − a| в Z,natAbs плюс 1.

LaTeX

$$|uIcc(a,b)| = |b − a|_{Z} + 1$$

Lean4

@[simp]
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1 := by rw [← Nat.card_uIcc, ← map_valEmbedding_uIcc, card_map]

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