card_Ioo_eq_card_Ico_sub_one — Mathlib

English

For any a,b, the cardinality of Ioo(a,b) equals the cardinality of 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 : α) : #(Ioo a b) = #(Ico a b) - 1 := by
  classical
  by_cases h : a < b
  · rw [Ico_eq_cons_Ioo h, card_cons]
    exact (Nat.add_sub_cancel _ _).symm
  · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

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