prod_range_natCast_sub — Mathlib

English

For a finite set s with a linear order, the product over i∈s of (1 − f(i)) equals 1 minus the sum over i∈s of f(i) times the product over j<i of (1 − f(j).

Русский

Для конечного множества s с линейным порядком произведение (1−f(i)) по i∈s равно 1 минус сумма по i∈s от f(i) на произведение по j<i (1−f(j)).

LaTeX

$$$\\prod_{i\\in s} (1 - f(i)) = 1 - \\sum_{i\\in s} f(i) \\prod_{j\\in s, j

Lean4

theorem prod_range_natCast_sub (n k : ℕ) : ∏ i ∈ range k, (n - i : R) = (∏ i ∈ range k, (n - i) : ℕ) :=
  by
  rw [prod_natCast]
  rcases le_or_gt k n with hkn | hnk
  · exact prod_congr rfl fun i hi => (Nat.cast_sub <| (mem_range.1 hi).le.trans hkn).symm
  · rw [← mem_range] at hnk
    rw [prod_eq_zero hnk, prod_eq_zero hnk] <;> simp

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