cfc_apply_of_not_predicate

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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

English

If p(a) is false, then cfc f a = 0 for any f. This is a corollary of the prior case when the predicate fails.

Русский

Если p(a) ложно, то для любого f выполняется cfc f a = 0.

LaTeX

$$$ \neg p(a) \Rightarrow cfc\, f\, a = 0 $$$

Lean4

theorem cfc_apply_of_not_predicate {f : R → R} (a : A) (ha : ¬p a) : cfc f a = 0 := by
  rw [cfc_def, dif_neg (not_and_of_not_left _ ha)]

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

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

Разделы

Аффилиация

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