cfcₙHom_predicate — Mathlib

English

If the element a satisfies the predicate p, then every value produced by the nonunital continuous functional calculus from a function f also satisfies p.

Русский

Если элемент a удовлетворяет предикату p, то каждый результат применения неприводимого непрерывного функционального калькулятора к a через функцию f удовлетворяет p.

LaTeX

$$$p\\bigl(\\mathrm{cfc}_{n}\mathrm{Hom}(ha)\\;f\\bigr)$$$

Lean4

theorem cfcₙHom_predicate (f : C(σₙ R a, R)₀) : p (cfcₙHom ha f) :=
  (NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate a ha).choose_spec.2.2.2 f

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