cfcₙ_apply_of_not_and_and

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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

← MathLib Explorer

English

If f(0) ≠ 0 then cfcₙ f a = 0.

Русский

Если f(0) не равно нулю, то cfcₙ f a равно нулю.

LaTeX

$$$f(0) \neq 0 \Rightarrow cfc_n f a = 0$$$

Lean4

theorem cfcₙ_apply_of_not_and_and {f : R → R} (a : A) (ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)) :
    cfcₙ f a = 0 := by rw [cfcₙ_def, dif_neg ha]

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

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

Разделы

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

Аффилиация

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