cfcₙ_apply_of_not_map_zero

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

URI: https://scilib.ai/kg/mathlib#cfcₙ_apply_of_not_map_zero

← MathLib Explorer

English

cfcₙ f a equals cfcₙL ha applied to mkD of the restricted f.

Русский

cfcₙ f a равно cfcₙL ha применённому к mkD ограниченного f.

LaTeX

$$$cfc_n f a = cfc_nL ha (mkD ((quasispectrum R a).restrict f) 0)$$$

Lean4

theorem cfcₙ_apply_of_not_map_zero {f : R → R} (a : A) (hf : ¬f 0 = 0) : cfcₙ f a = 0 := by
  rw [cfcₙ_def, dif_neg (not_and_of_not_right _ (not_and_of_not_right _ hf))]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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