card_Ioo_eq_card_Ico_sub_one — Mathlib

English

For any a,b in a locally finite order, the number of elements in Ioo(a,b) equals the number of elements in Ico(a,b) minus 1.

Русский

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

LaTeX

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

Lean4

theorem card_Ioo_eq_card_Ico_sub_one (a b : α) : card (Ioo a b) = card (Ico a b) - 1 :=
  Finset.card_Ioo_eq_card_Ico_sub_one _ _

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