sum_boole — Mathlib

English

The natural number cast of the cardinality of the subfamily defined by a predicate p equals the sum over s of 1 when p holds and 0 otherwise.

Русский

Натуральное число, приводимое к полю R, кардинальности подмножества {x ∈ s | p x} равно сумме по s единиц, когда p выполняется, и нуля иначе.

LaTeX

$$$$ \\left( \\#\\{x \\in s \\mid p(x)\\} \\right) : R = \\sum_{a \\in s} \\mathbf{1}_{p(a)}. $$$$

Lean4

@[simp]
theorem sum_boole (p) [DecidablePred p] (s : Finset ι) : (∑ x ∈ s, if p x then 1 else 0 : R) = #({x ∈ s | p x}) :=
  (natCast_card_filter _ _).symm

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