cfc_const_one

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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

English

cfc of the constant function 1 at a equals 1.

Русский

cfc единицы в a равен единице.

LaTeX

$$cfc(\,1\, : R \to R) a = 1$$

Lean4

theorem cfc_const_one : cfc (fun _ : R ↦ 1) a = 1 :=
  cfc_one R a

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

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

Разделы

Аффилиация

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