cfc_predicate_one

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

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

English

For unit element 1, p(1).

Русский

Для единицы v: p(1).

LaTeX

$$p(1)$$

Lean4

theorem cfc_predicate_one : p 1 :=
  map_one (algebraMap R A) ▸ cfc_predicate_algebraMap (1 : R)

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

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

Разделы

Аффилиация

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