countP_nsmul — Mathlib

English

For any predicate p and multiset s, countP p (n • s) = n · countP p s, i.e., the number of elements satisfying p scales additively with n.

Русский

Для любого предиката p и мультимножества s имеет место countP p (n • s) = n · countP p s; число элементов, удовлетворяющих p, растет линейно с умножением n.

LaTeX

$$$\operatorname{countP} p (n \cdot s) = n \cdot \operatorname{countP} p s.$$$

Lean4

@[simp]
theorem countP_nsmul (s) (n : ℕ) : countP p (n • s) = n * countP p s := by
  induction n <;> simp [*, succ_nsmul, succ_mul, zero_nsmul]

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