tprod_bool — Mathlib

English

For a function f: Bool → α, the tprod over Bool equals the product f(false) ⋅ f(true): ∏' i Bool, f(i) = f(false) · f(true).

Русский

Для функции f: Булево → α т-произведение над булевыми равно произведению f(ложь) и f(истина): ∏' i ∈ Bool, f(i) = f(false) · f(true).

LaTeX

$$$\\\\prod' i:Bool \\, f(i) = f(False) \\\\cdot f(True)$$$

Lean4

@[to_additive]
theorem tprod_bool (f : Bool → α) : ∏' i : Bool, f i = f false * f true := by
  rw [tprod_fintype, Fintype.prod_bool, mul_comm]

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