card_Ico_eq_card_Icc_sub_one — Mathlib

English

For any a,b in a locally finite order, the number of elements in the half-open interval Ico(a,b) is one less than the number of elements in the closed interval Icc(a,b).

Русский

Для любых a, b в локально конечном порядке число элементов в полузакрытом интервале Ico(a,b) меньше числа элементов в замкнутом интервале Icc(a,b) на 1.

LaTeX

$$$ |Ico(a,b)| = |Icc(a,b)| - 1 $$$

Lean4

theorem card_Ico_eq_card_Icc_sub_one (a b : α) : card (Ico a b) = card (Icc a b) - 1 :=
  Finset.card_Ico_eq_card_Icc_sub_one _ _

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