prod_Ioi_mul_eq_prod_Ici — Mathlib

English

Let α be as above and f: α → M. Then the product over x > a, multiplied by f(a), equals the product over x ≥ a; i.e., ∏_{x ∈ Ioi(a)} f(x) · f(a) = ∏_{x ∈ Ici(a)} f(x).

Русский

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

LaTeX

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

Lean4

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

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