card_Iic — Mathlib

English

For DecidableEq α, the card of Finset.Iic s equals the product over i in s.toFinset of (s.count i + 1).

Русский

Для декадируемого равенства верно: |Finset.Iic s| = ∏_{i ∈ s.toFinset} (s.count i + 1).

LaTeX

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

Lean4

theorem card_Iic : (Finset.Iic s).card = ∏ i ∈ s.toFinset, (s.count i + 1) := by
  simp_rw [Iic_eq_Icc, card_Icc, bot_eq_zero, toFinset_zero, empty_union, count_zero, tsub_zero]

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