log — Mathlib

English

If a is self-adjoint, then log(a) is self-adjoint as well (log preserves self-adjointness under the continuous functional calculus).

Русский

Если a самосопряжённо, то log(a) также самосопряжённо (логарифм сохраняет самосопряжённость через непрерывный функциональный калькулятор).

LaTeX

$$$\text{IsSelfAdjoint}(\log(a))$$$

Lean4

@[simp, grind]
protected theorem _root_.IsSelfAdjoint.log {a : A} : IsSelfAdjoint (log a) :=
  cfc_predicate _ a

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