cfc_apply_mem_elemental — Mathlib

English

For any function f, the element produced by cfc is in the elemental subalgebra generated by a.

Русский

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

LaTeX

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

Lean4

@[simp, grind ←]
theorem cfc_apply_mem_elemental (f : 𝕜 → 𝕜) (a : A) : cfc f a ∈ elemental 𝕜 a :=
  cfc_cases _ a f (zero_mem _) fun hf ha ↦ cfcHom_apply_mem_elemental ha ⟨_, hf.restrict⟩

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