mul_prod_Iio_eq_prod_Iic — Mathlib

English

Let α be a locally finite order with bottom element, and f: α → M into a commutative monoid M. Then f(a) · ∏_{x ∈ Iio(a)} f(x) = ∏_{x ∈ Iic(a)} f(x).

Русский

Пусть α — локально конечный упорядоченный множество с нижней границей, и f: α → M. Тогда f(a) умножить на произведение по x < a равно произведению по x ≤ a.

LaTeX

$$$ f(a) \cdot \prod_{x \in \mathrm{Iio}(a)} f(x) = \prod_{x \in \mathrm{Iic}(a)} f(x) $$$

Lean4

@[to_additive]
theorem mul_prod_Iio_eq_prod_Iic (a : α) : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x := by
  rw [Iic_eq_cons_Iio, prod_cons]

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