isPositive_adjoint_comp_self

Mathlib.Analysis.InnerProductSpace.Positive

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.isPositive_adjoint_comp_self

English

The operator S† ∘ T ∘ S is positive when T is positive.

Русский

Оператор S† ∘ T ∘ S положителен, если T положителен.

LaTeX

$$$ (S^\dagger \circ T \circ S) .IsPositive$$$

Lean4

theorem isPositive_adjoint_comp_self (S : E →L[𝕜] F) : (S† ∘L S).IsPositive := by
  simpa using isPositive_one.adjoint_conj S

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

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

Разделы

Аффилиация

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