English
Let e: ι → κ be such that e is injective on s and maps s into t. If for all i ∈ s, f i = g (e i) and the remaining g-values on t away from image e(s) give 1, then the product over s of f equals the product over t of g.
Русский
Пусть e: ι → κ таково, что на s функция инъективна и образуется в t. Если для всех i ∈ s выполнено f(i) = g(e(i)) и для остальных элементов t вне образа e(s) значения g равны 1, тогда произведение по s функций f равно произведению по t функций g.
LaTeX
$$$\forall e:\, \iota \to \kappa,\; \text{InjOn}(e,s) \to \text{MapsTo}(e,s,t) \to (\forall i\in t, i\notin e''s \to g(i)=1) \to (\forall i\in s, f(i)=g(e(i))) \to \prod_{i\in s} f(i) = \prod_{j\in t} g(j)$$$
Lean4
@[to_additive]
theorem prod_of_injOn (e : ι → κ) (he : Set.InjOn e s) (hest : Set.MapsTo e s t) (h' : ∀ i ∈ t, i ∉ e '' s → g i = 1)
(h : ∀ i ∈ s, f i = g (e i)) : ∏ i ∈ s, f i = ∏ j ∈ t, g j := by
classical
exact
(prod_nbij e (fun a ↦ mem_image_of_mem e) he (by simp [Set.surjOn_image]) h).trans <|
prod_subset (image_subset_iff.2 hest) <| by simpa using h'
