rpow_sum_of_pos — Mathlib

English

For any real a > 0, any index set ι, any function f: ι → ℝ, and any finite set s ⊆ ι, a^(∑_{x∈s} f(x)) = ∏_{x∈s} a^(f(x)).

Русский

Пусть a > 0, ι — множество индексов, f:ι → ℝ, и s — конечное подмножество ι. Тогда a^{∑_{x∈s} f(x)} = ∏_{x∈s} a^{f(x)}.

LaTeX

$$$\forall ι\,\forall a>0\,\forall f:ι \to \mathbb{R}\,\forall s\in Finset(ι):\ (a^{\sum_{x\in s} f(x)}) = \prod_{x\in s} a^{f(x)}$$$

Lean4

theorem rpow_sum_of_pos {ι : Type*} {a : ℝ} (ha : 0 < a) (f : ι → ℝ) (s : Finset ι) :
    (a ^ ∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x :=
  map_sum (⟨⟨fun (x : ℝ) => (a ^ x : ℝ), rpow_zero a⟩, rpow_add ha⟩ : ℝ →+ (Additive ℝ)) f s

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