cfc_const_zero

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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

English

cfc of the zero function at a is zero: cfc 0 a = 0.

Русский

Нуль-функция в cfc: cfc 0 a = 0.

LaTeX

$$cfc(0 : R \to R) a = 0$$

Lean4

@[simp]
theorem cfc_const_zero : cfc (fun _ : R ↦ 0) a = 0 :=
  cfc_zero R a

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

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

Разделы

Аффилиация

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