English
Updating the input at index j in x to x_j updates exp 𝕂 x accordingly: exp 𝕂 (Function.update x j x_j) = Function.update (exp 𝕂 x) j (exp 𝕂 x_j).
Русский
При замене значения по индексу j в x на x_j экспонента изменяется согласно: exp 𝕂 (Function.update x j x_j) = Function.update (exp 𝕂 x) j (exp 𝕂 x_j).
LaTeX
$$$\\;\\text{Function.update} (\\exp 𝕂 x) j (\\exp 𝕂 x_j) = \\exp 𝕂 (\\text{Function.update} x j x_j)$$$
Lean4
theorem _root_.Function.update_exp {ι : Type*} {𝔸 : ι → Type*} [Finite ι] [DecidableEq ι] [∀ i, NormedRing (𝔸 i)]
[∀ i, NormedAlgebra 𝕂 (𝔸 i)] [∀ i, CompleteSpace (𝔸 i)] (x : ∀ i, 𝔸 i) (j : ι) (xj : 𝔸 j) :
Function.update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (Function.update x j xj) :=
by
ext i
simp_rw [Pi.exp_def]
exact (Function.apply_update (fun i => exp 𝕂) x j xj i).symm
