cfc_star — Mathlib

English

If r ∈ R, the spectrum of the algebra map algebraMap R A r is {r} provided A is nontrivial.

Русский

Если r ∈ R, спектр алгебраической карты algebraMap R A r равен {r} при условии не тривиальности A.

LaTeX

$$$ spectrum\; R\; (algebraMap\; R A\; r) = \{ r \}$$$

Lean4

theorem cfc_star (f : R → R) (a : A) : cfc (fun x ↦ star (f x)) a = star (cfc f a) :=
  by
  by_cases h : p a ∧ ContinuousOn f (spectrum R a)
  · obtain ⟨ha, hf⟩ := h
    rw [cfc_apply f a, ← map_star, cfc_apply _ a]
    congr
  · obtain (ha | hf) := not_and_or.mp h
    · simp [cfc_apply_of_not_predicate a ha]
    · rw [cfc_apply_of_not_continuousOn a hf, cfc_apply_of_not_continuousOn, star_zero]
      exact fun hf_star ↦ hf <| by simpa using hf_star.star

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