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]