card_Ioc_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 Ioc(a,b) equals the number of elements in Icc(a,b) minus 1.

Русский

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

LaTeX

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

Lean4

theorem card_Ioc_eq_card_Icc_sub_one (a b : α) : card (Ioc a b) = card (Icc a b) - 1 :=
  Finset.card_Ioc_eq_card_Icc_sub_one _ _

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