isSelfAdjoint_map — Mathlib

English

In a star-powered functor setting, the image of a self-adjoint element under any star-preserving map is self-adjoint.

Русский

Образ самосопряжённого элемента под любую карту, сохраняющую звезду, самосопряжён.

LaTeX

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

Lean4

theorem _root_.isSelfAdjoint_map {F R S : Type*} [Star R] [Star S] [FunLike F R S] [StarHomClass F R S] [TrivialStar R]
    (f : F) (x : R) : IsSelfAdjoint (f x) :=
  (IsSelfAdjoint.all x).map f

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