card_Ioo — Mathlib

English

The cardinality of Finset.Ioo s t equals the Icc cardinality minus 2: #(Finset.Ioo s t) = card_Icc s t − 2.

Русский

Число элементов Finset.Ioo s t равно кардинальности Icc минус 2.

LaTeX

$$$\\#(\\mathrm{Finset}.Ioo\\ s\\ t) = \\#(\\mathrm{Finset}.Icc\\ s\\ t) - 2$$$

Lean4

theorem card_Ioo : #(Finset.Ioo s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) - 2 := by
  rw [Finset.card_Ioo_eq_card_Icc_sub_two, card_Icc]

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