prod_Iio_mul_eq_prod_Iic — Mathlib

English

Let α be as above and f: α → M. Then (∏_{x ∈ Iio(a)} f(x)) · f(a) = ∏_{x ∈ Iic(a)} f(x).

Русский

Пусть α удовлетворяет условиям, и f: α → M. Тогда (∏_{x ∈ Iio(a)} f(x)) · f(a) = ∏_{x ∈ Iic(a)} f(x).

LaTeX

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

Lean4

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

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