posPart_eq_zero_of_not_isSelfAdjoint

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

URI: https://scilib.ai/kg/mathlib#CFC.posPart_eq_zero_of_not_isSelfAdjoint

English

If a is not self-adjoint, then a⁺ = 0.

Русский

Если a не самосопряжённо, то a⁺ = 0.

LaTeX

$$$\neg IsSelfAdjoint(a) \Rightarrow a^+ = 0$$$

Lean4

theorem posPart_eq_zero_of_not_isSelfAdjoint {a : A} (ha : ¬IsSelfAdjoint a) : a⁺ = 0 :=
  cfcₙ_apply_of_not_predicate a ha

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

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

Разделы

Аффилиация

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