prod_preimage — Mathlib

English

Let f: ι → κ, s finite in κ, hf injOn preimage-source, g: κ → β; if ∀ x∈s, x ∉ range f → g x = 1, then ∏ x∈s.preimage f hf, g(f x) = ∏ x∈s, g x.

Русский

Пусть f: ι → κ, s конечное над κ, hf, g: κ → β; если ∀ x∈s, x ∉ range f → g x = 1, тогда ∏_{x∈s.preimage f} g(f x) = ∏_{x∈s} g(x).

LaTeX

$$$\\displaystyle \\prod_{x \\in s.\\mathrm{preimage}(f) hf} g(f x) = \\prod_{x \\in s} g(x)$, при условии $\\forall x \\in s, x \\notin \\mathrm{range}(f) \\Rightarrow g(x) = 1$$$

Lean4

@[to_additive]
theorem prod_preimage (f : ι → κ) (s : Finset κ) (hf) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) :
    ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x := by
  classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

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