card_fintype_Icc — Mathlib

English

The set Icc(a,b) has the expected finite cardinal: the number of elements in Set.Icc(a,b) equals the natural expression for the length of the interval.

Русский

У множества Icc(a,b) конечный кардинал, равный длине интервала в явном виде.

LaTeX

$$$|\\mathrm{Set.Icc}(a,b)| = \\max\\{0,\, b - a + 1\\}$$$

Lean4

@[deprecated Fintype.card_Icc (since := "2025-03-28")]
theorem card_fintype_Icc : Fintype.card (Set.Icc a b) = (b + 1 - a).toNat := by simp

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