cfcₙ_predicate

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

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

English

Predicate zero property is preserved by the calculus at zero input.

Русский

Свойство нуля предиката сохраняется калькулятором при нулевом входе.

LaTeX

$$p 0$$

Lean4

theorem cfcₙ_predicate (f : R → R) (a : A) : p (cfcₙ f a) :=
  cfcₙ_cases p a f (cfcₙ_predicate_zero R) fun _ _ _ ↦ cfcₙHom_predicate ..

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

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

Разделы

Аффилиация

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