cfcₙHom_nonneg_iff — Mathlib

English

The map cfc_nHomSuperset ha hs is continuous.

Русский

Отображение cfc_nHomSuperset ha hs непрерывно.

LaTeX

$$$$ \\text{Continuous}(\\mathrm{cfc\\!}_nHomSuperset\\ ha\\ hs) $$$$

Lean4

theorem cfcₙHom_nonneg_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(σₙ R a, R)₀} :
    0 ≤ cfcₙHom ha f ↔ 0 ≤ f := by
  constructor
  ·
    exact fun hf x ↦
      (cfcₙHom_map_quasispectrum ha (R := R) _ ▸ quasispectrum_nonneg_of_nonneg (cfcₙHom ha f) hf) _ ⟨x, rfl⟩
  · simpa using (cfcₙHom_mono ha (f := 0) (g := f) ·)

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