commute_cfcHom — Mathlib

English

If a is self-adjoint, and b commutes with a, then for every continuous functional calculus f, cfcHom ha f commutes with b.

Русский

Если a является самосопряженным и b коммутирует с a, то для любого непрерывного функционального калькулятора f элемент cfcHom ha f коммутиравен с b.

LaTeX

$$$\forall a,b \in A,\ ha : p(a)\, IsSelfAdjoint(a)\,\Commute(a,b)\Rightarrow \forall f \in C(\mathrm{spectrum}(\mathbb{K},a),\mathbb{K}),\ Commute( cfcHom(ha,f), b).$$

Lean4

protected theorem commute_cfcHom {a b : A} (ha : p a) (ha' : IsSelfAdjoint a) (hb : Commute a b)
    (f : C(spectrum 𝕜 a, 𝕜)) : Commute (cfcHom ha f) b :=
  hb.cfcHom ha (ha'.star_eq.symm ▸ hb) f

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