map — Mathlib

English

If x is self-adjoint and f is a star-homomorphism (a function-like structure preserving star), then f(x) is self-adjoint.

Русский

Если x самосопряжён, и f — звездо-гомоморфизм, то f(x) самосопряжён.

LaTeX

$$$\text{IsSelfAdjoint}(x) \rightarrow \text{IsSelfAdjoint}(f\,x)$$$

Lean4

/-- Functions in a `StarHomClass` preserve self-adjoint elements. -/
@[aesop 10% apply]
theorem map {F R S : Type*} [Star R] [Star S] [FunLike F R S] [StarHomClass F R S] {x : R} (hx : IsSelfAdjoint x)
    (f : F) : IsSelfAdjoint (f x) :=
  show star (f x) = f x from map_star f x ▸ congr_arg f hx

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