card_Icc — Mathlib

English

The cardinality of Finset.Icc s t equals the product over i in s.toFinset ∪ t.toFinset of (t.count i + 1 - s.count i).

Русский

Число элементов Finset.Icc s t равно произведению по i из объединения s и t: (t.count i + 1 - s.count i).

LaTeX

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

Lean4

theorem card_Icc : #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i) := by
  simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply, toDFinsupp_support]

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