range_cfcₙ_eq_range_cfcₙHom — Mathlib

English

For a ∈ A with p(a), the image of the map f ↦ cfc_n f a is exactly the range of the nonunital hom cfc_nHom ha.

Русский

Для a ∈ A с p(a) образ отображения f ↦ cfc_n f a совпадает с образом соответствующего неопустимого гомоморфизма.

LaTeX

$$$$ \\operatorname{Range}(f \\mapsto cfc\\!_n f\\,a) = \\operatorname{Range}(cfc\\!_nHom\\ ha) $$$$

Lean4

theorem range_cfcₙ_eq_range_cfcₙHom {a : A} (ha : p a) :
    Set.range (cfcₙ (R := R) · a) = NonUnitalStarAlgHom.range (cfcₙHom ha (R := R)) :=
  by
  ext
  constructor
  all_goals rintro ⟨f, rfl⟩
  · exact cfcₙ_cases _ a f (zero_mem _) fun hf hf₀ ha ↦ ⟨_, rfl⟩
  · exact ⟨Subtype.val.extend f 0, cfcₙHom_eq_cfcₙ_extend _ ha _ |>.symm⟩

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