exp_def — Mathlib

English

The exponential on a product indexed by ι equals the product of exponentials componentwise: exp 𝕂 x = (i ↦ exp 𝕂 (x i)).

Русский

Экспонента над функцией ι → 𝔸 равна произведению экспонент по компонентам: exp 𝕂 x = (i ↦ exp 𝕂 (x i)).

LaTeX

$$$\\exp 𝕂 x = \\big( i \\mapsto \\exp 𝕂 (x(i)) \\big)$$$

Lean4

theorem _root_.Pi.exp_def {ι : Type*} {𝔸 : ι → Type*} [Finite ι] [∀ i, NormedRing (𝔸 i)] [∀ i, NormedAlgebra 𝕂 (𝔸 i)]
    [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i) : exp 𝕂 x = fun i => exp 𝕂 (x i) :=
  funext <| Pi.coe_exp 𝕂 x

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