card_uIcc — Mathlib

English

The size of the symmetric closed interval between a and b equals |b−a|ℤ natAbs plus 1.

Русский

Размер симметричного замкнутого интервала между a и b равен |b−a| по целым числам, взятому по модулю, плюс 1.

LaTeX

$$$\forall a,b \in \mathbb{N},\ |\mathrm{uIcc}(a,b)\rvert = (|b - a|_{\mathbb{Z}}).natAbs + 1$$$

Lean4

@[simp]
theorem card_uIcc : #(uIcc a b) = (b - a : ℤ).natAbs + 1 :=
  (card_Icc _ _).trans <| by rw [← Int.natCast_inj, Int.ofNat_sub] <;> omega

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