range_cfc — Mathlib

English

As above, the range of the continuous functional calculus applied to a is exactly the subalgebra generated by a.

Русский

Как и выше, образ непрерывного функционального калькулятора на a равен подалгебре, порождённой a.

LaTeX

$$$\\mathrm{range}(\\mathrm{cfc}\\; a) = \\langle a \\rangle$$$

Lean4

theorem range_cfc {a : A} (ha : p a) : Set.range (cfc (R := 𝕜) · a) = elemental 𝕜 a := by
  rw [range_cfc_eq_range_cfcHom 𝕜 ha, range_cfcHom 𝕜 ha]

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