hasProd_range_iff — Mathlib

English

If g is injective, then HasProd on the range of g with respect to f is equivalent to HasProd of the composed function f∘g.

Русский

Если g инъективна, HasProd на диапазоне g относительно f эквивалентен HasProd от композиции f∘g.

LaTeX

$$$\text{Injective } g \Rightarrow \text{HasProd } (f \circ g) a \iff \text{HasProd } (f x) (a) \text{ по } x \in \operatorname{range}(g)$$$

Lean4

@[to_additive]
theorem hasProd_range_iff {g : γ → β} (hg : Injective g) : HasProd (fun x : Set.range g ↦ f x) a ↔ HasProd (f ∘ g) a :=
  (Equiv.ofInjective g hg).hasProd_iff.symm

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