card_uIcc — Mathlib

English

The cardinality of uIcc s t equals the product over i in s.toFinset ∪ t.toFinset of (natAbs(t.count i − s.count i) + 1).

Русский

Число элементов uIcc s t равно произведению по i ∈ s∪t от (|t.count i − s.count i| + 1).

LaTeX

$$$\\#(\\mathrm{uIcc}\\ s\\ t) = \\prod_{i \\in s.toFinset \\cup t.toFinset} \\big(\\lvert t.count(i) - s.count(i) \\rvert_{\\mathbb{Z}}.natAbs + 1\\big)$$$

Lean4

theorem card_uIcc : (uIcc s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, ((t.count i - s.count i : ℤ).natAbs + 1) := by
  simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply, toDFinsupp_support]

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