tprod_image — Mathlib

English

For an injective g: γ → β, ∏' x : Set.range g, f x = ∏' x, f (g x).

Русский

При инъекции g: γ → β выполняется т-произведение по диапазону: ∏' x : Set.range g, f x = ∏' x, f(g x).

LaTeX

$$$\\\\prod' x : Set.range g, f x = \\\\prod' x, f (g x)$$$

Lean4

@[to_additive]
theorem tprod_image {g : γ → β} (f : β → α) {s : Set γ} (hg : Set.InjOn g s) : ∏' x : g '' s, f x = ∏' x : s, f (g x) :=
  ((Equiv.Set.imageOfInjOn _ _ hg).tprod_eq fun x ↦ f x).symm

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