cfc_apply_one — Mathlib

English

Similarly, the functional calculus at the identity yields the algebra-map image of f(1).

Русский

Аналогично, применение функционального вычисления к единице даёт образ через алгебраическое отображение f(1).

LaTeX

$$$ cfc\, f\; (1_A) = \ algebraMap\ R\ A\ (f(1)) $$$

Lean4

@[simp]
theorem cfc_apply_one {f : R → R} : cfc f (1 : A) = algebraMap R A (f 1) := by simpa using cfc_algebraMap (A := A) 1 f

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