cfcHom_apply_mem_elemental — Mathlib

English

For ha, f, the image under the functional calculus lies in the elemental subalgebra generated by a.

Русский

Для ha, f образ под функциональным калькулятором принадлежит элементальной подалгебре, порождённой a.

LaTeX

$$$cfc\\, ha\\, f \\in \\text{elemental }\\; a$$$

Lean4

theorem cfcHom_apply_mem_elemental {a : A} (ha : p a) (f : C(spectrum 𝕜 a, 𝕜)) : cfcHom ha f ∈ elemental 𝕜 a :=
  range_cfcHom 𝕜 ha ▸ ⟨f, rfl⟩

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