finprod_emb_domain — Mathlib

English

Similarly to emb_domain', for an embedding f : α ↪ β, the finprod over β of the piecewise defined g equals the finprod over α of g.

Русский

Аналогично emb_domain', для вложения f : α ↪ β, финпроизведение по β эквивалентно по α.

LaTeX

$$$ finprod f \\;=\; finprod g $$$

Lean4

@[to_additive]
theorem finprod_emb_domain (f : α ↪ β) [DecidablePred (· ∈ Set.range f)] (g : α → M) :
    (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a :=
  finprod_emb_domain' f.injective g

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