cfc_predicate

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

URI: https://scilib.ai/kg/mathlib#cfc_predicate

English

For any f, a, the property p is maintained by cfc f a: p(cfc f a).

Русский

Для любого f, a свойство p сохраняется под применением cfc: p(cfc f a).

LaTeX

$$p(cfc f a)$$

Lean4

theorem cfc_predicate (f : R → R) (a : A) : p (cfc f a) :=
  cfc_cases p a f (cfc_predicate_zero R) fun _ _ ↦ cfcHom_predicate ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru