apply_le_of_isSelfAdjoint — Mathlib

English

If f is a positive linear map between C*-algebras and x is self-adjoint, then the norm of f(x) is controlled by the norm of f(1) times the norm of x.

Русский

Если f — положительное линейное отображение между C*-алгебрами, и x — самосопряжённый, тогда нормa f(x) не превышает норму f(1) умноженную на норму x.

LaTeX

$$$\|f(x)\| \le \|f(1)\| \cdot \|x\|$ for self-adjoint x and positive f$$

Lean4

theorem apply_le_of_isSelfAdjoint (f : B₁ →ₚ[ℂ] B₂) (x : B₁) (hx : IsSelfAdjoint x) : f x ≤ f (algebraMap ℝ B₁ ‖x‖) :=
  by
  gcongr
  exact IsSelfAdjoint.le_algebraMap_norm_self hx

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