card_Ioo_eq_card_Icc_sub_two — 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 Icc(a,b) minus 2.

Русский

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

LaTeX

$$$ |Ioo(a,b)| = |Icc(a,b)| - 2 $$$

Lean4

theorem card_Ioo_eq_card_Icc_sub_two (a b : α) : card (Ioo a b) = card (Icc a b) - 2 :=
  Finset.card_Ioo_eq_card_Icc_sub_two _ _

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