cfcHom_isStrictlyPositive_iff — Mathlib

English

Compose cfcHom with a superset embedding to a larger spectrum, yielding a star-algebra homomorphism from C(s, R) to A.

Русский

Сочетание cfcHom с гомоморфизмом вложения в больший спектр даёт гомоморфизм от C(s,R) в A.

LaTeX

$$cfcHom ha |>.comp (ContinuousMap.compStarAlgHom' R R ⟨_, _⟩) : C(s, R) →⋆ₐ[R] A$$

Lean4

theorem cfcHom_isStrictlyPositive_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(spectrum R a, R)} :
    IsStrictlyPositive (cfcHom ha f) ↔ ∀ x, 0 < f x :=
  by
  refine
    ⟨fun hf x => hf.spectrum_pos <| cfcHom_map_spectrum (R := R) ha _ ▸ Set.mem_range_self x, fun h =>
      ⟨cfcHom_nonneg_iff _ |>.mpr fun x => le_of_lt (h x), ?_⟩⟩
  apply spectrum.isUnit_of_zero_notMem (R := R)
  grind [cfcHom_map_spectrum, ne_of_lt]

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