card_Ico — Mathlib

English

The cardinality of Finset.Ico s t equals the corresponding product minus 1: #(Finset.Ico s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) − 1.

Русский

Число элементов Finset.Ico s t равно произведению минус единица.

LaTeX

$$$\\#(\\mathrm{Finset}.Ico\\ s\\ t) = \\prod_{i \\in s.toFinset \\cup t.toFinset} \\big( t.count(i) + 1 - s.count(i) \\big) - 1$$$

Lean4

theorem card_Ico : #(Finset.Ico s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) - 1 := by
  rw [Finset.card_Ico_eq_card_Icc_sub_one, card_Icc]

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