prod_of_injective — Mathlib

English

Let e: ι → κ be injective, with f: ι → M and g: κ → M, h' ensures g equals 1 off the range of e, and h ensures f(i) = g(e(i)) for all i. Then ∏ i f i = ∏ j g j.

Русский

Пусть e — инъекция, f: ι → M, g: κ → M, и выполнены условия h' и h; тогда произведение по i f i равно произведению по j g j.

LaTeX

$$$$\\prod_{i} f(i) = \\prod_{j} g(j)$$$$

Lean4

@[to_additive]
theorem prod_of_injective (e : ι → κ) (he : Injective e) (f : ι → M) (g : κ → M) (h' : ∀ i ∉ Set.range e, g i = 1)
    (h : ∀ i, f i = g (e i)) : ∏ i, f i = ∏ j, g j :=
  prod_of_injOn e he.injOn (by simp) (by simpa using h') (fun i _ ↦ h i)

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