cfc — Mathlib

English

The output of the continuous functional calculus is self-adjoint for any used f and a, i.e., cfc f a is self-adjoint.

Русский

Вывод непрерывного функционального вычисления является самосопряжённым: cfc f a самосопряжённый элемент.

LaTeX

$$IsSelfAdjoint (cfc f a)$$

Lean4

@[simp]
protected theorem cfc [ContinuousFunctionalCalculus R A IsSelfAdjoint] {f : R → R} {a : A} : IsSelfAdjoint (cfc f a) :=
  cfc_predicate _ _

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