mul_prod_Ioi_eq_prod_Ici — Mathlib

English

Let α be a locally finite ordered set with a top element, and M a commutative monoid. For any a ∈ α and any function f: α → M, the product of f over all elements greater than a, multiplied by f(a), equals the product of f over all elements greater than or equal to a; i.e., ∏_{x ∈ Ici(a)} f(x) = f(a) · ∏_{x ∈ Ioi(a)} f(x).

Русский

Пусть α — локально конечное упорядоченное множество с верхней границей, M — коммутативная moноида, и функция f: α → M. Тогда для любого a ∈ α выполняется равенство: ∏_{x ∈ Ici(a)} f(x) = f(a) · ∏_{x ∈ Ioi(a)} f(x).

LaTeX

$$$ f(a) \cdot \prod_{x \in \mathrm{Ioi}(a)} f(x) = \prod_{x \in \mathrm{Ici}(a)} f(x) $$$

Lean4

@[to_additive]
theorem mul_prod_Ioi_eq_prod_Ici (a : α) : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x := by
  rw [Ici_eq_cons_Ioi, prod_cons]

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