card_Ico_eq_card_Icc_sub_one — Mathlib

English

For any a,b, the cardinality of Ico(a,b) equals the cardinality of Icc(a,b) minus 1.

Русский

Для любых 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 : α) : #(Ico a b) = #(Icc a b) - 1 := by
  classical
  by_cases h : a ≤ b
  · rw [Icc_eq_cons_Ico h, card_cons]
    exact (Nat.add_sub_cancel _ _).symm
  · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]

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