tprod_fintype — Mathlib

English

If L is a LeAtTop filter and β is finite, then the tprod over L of a function f: β → α equals the ordinary finite product over β: ∏'_{L} b, f(b) = ∏_{b ∈ β} f(b).

Русский

Пусть L — фильтр LeAtTop, β — конечный. Тогда т-произведение по L функции f: β → α равно обычному конечному произведению по β: ∏'_L b, f(b) = ∏_{b ∈ β} f(b).

LaTeX

$$$\\\\prod'_{L} b \\, f(b) = \\\\prod_{b \\in \\beta} f(b)$$$

Lean4

@[to_additive]
theorem tprod_fintype [L.LeAtTop] [Fintype β] (f : β → α) : ∏'[L] b, f b = ∏ b, f b := by apply tprod_eq_prod; simp

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