English
Let R be a commutative semiring, A a suitable nonunital R-algebra with a predicate p on A, and a ∈ A such that p(a) holds. Suppose f,g: R → R are functions continuous on the quasispectrum σ_n(R,a) and satisfy f(0) = g(0) = 0. Then the nonunital functional calculus is multiplicative on a:\n(cfc_n (x ↦ f(x) · g(x))) a = (cfc_n f a) · (cfc_n g a).
Русский
Пусть R — коммутативная полукольцо, A — подходящая некоприводимая по отношению к R алгебра, задано предикат p на A и элемент a ∈ A с условием p(a). Пусть f,g: R → R являются функциями, непрерывными на предмножество спектра σ_n(R,a) и удовлетворяют f(0) = g(0) = 0. Тогда неконунитальный функциональный калькулятор умножения удовлетворяет: cfc_n (x ↦ f(x)·g(x)) применимо к a равно произведению cfc_n f a и cfc_n g a.
LaTeX
$$$$\\text{If } p(a), \\ f,g:\\mathbb{R}\\to\\mathbb{R} \\text{ are continuous on } \\sigma_n(R,a) \\text{ and } f(0)=g(0)=0, \\\\ cfc\\!_n(\\,x\\mapsto f(x)\\,\\cdot\\, g(x)\\,)\\,a \;=\; cfc\\!_n f\\;a \\cdot cfc\\!_n g\\;a.$$$$
Lean4
theorem cfcₙ_mul : cfcₙ (fun x ↦ f x * g x) a = cfcₙ f a * cfcₙ g a :=
by
by_cases ha : p a
· rw [cfcₙ_apply f a, cfcₙ_apply g a, ← map_mul, cfcₙ_apply _ a]
congr
· simp [cfcₙ_apply_of_not_predicate a ha]
