map_isSelfAdjoint — Mathlib

English

A positive linear map sends self-adjoint elements to self-adjoint elements.

Русский

Положительное линейное отображение отправляет самосопряжённые элементы в самосопряжённые.

LaTeX

$$$f: A_1 \to A_2 \text{ positive linear map; } a \text{ self-adjoint} \Rightarrow f(a) \text{ self-adjoint}$$$

Lean4

@[aesop safe apply (rule_sets := [CStarAlgebra])]
theorem map_isSelfAdjoint (f : A₁ →ₚ[ℂ] A₂) (a : A₁) (ha : IsSelfAdjoint a) : IsSelfAdjoint (f a) :=
  by
  rw [← CFC.posPart_sub_negPart a ha]
  cfc_tac

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