commute_cfcₙHom — Mathlib

English

If a is self-adjoint and commutes with b, then cfcₙHom ha f commutes with b for all f.

Русский

Если a самосопряжено и коммутирует с b, то cfcₙHom ha f коммутирует с b для любого f.

LaTeX

$$$\forall a,b:\ IsSelfAdjoint(a) \land Commute(a,b) \Rightarrow \forall f:\, C(quasispectrum 𝕜 a, 𝕜)_0,\ Commute( cfcₙHom ha f, b).$$

Lean4

protected theorem commute_cfcₙHom {a b : A} (ha : p a) (ha' : IsSelfAdjoint a) (hb : Commute a b)
    (f : C(quasispectrum 𝕜 a, 𝕜)₀) : Commute (cfcₙHom ha f) b :=
  hb.cfcₙHom ha (ha'.star_eq.symm ▸ hb) f

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