range_cfcₙ_nnreal_eq_image_cfcₙ_real

English

For any a with a ≥ 0, the NNReal-range of cfc is equal to the image of cfc under real-valued functional calculus on spectrum a.

Русский

Для a ≥ 0 NNReal-образ cfc равен изображению cfc через вещественный функциональный калькулятор над спектром a.

LaTeX

$$$\\mathrm{range}(\\mathrm{cfc\\,nnreal}\\; a) = \\mathrm{image}\\; (\\mathrm{cfc}\\; a)\\{f \\mid \\forall x \\in \\mathrm{spectrum}(a), f(x) \\ge 0\\}$$$

Lean4

theorem range_cfcₙ_nnreal_eq_image_cfcₙ_real (a : A) (ha : 0 ≤ a) :
    Set.range (cfcₙ (R := ℝ≥0) · a) = (cfcₙ · a) '' {f | ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x} :=
  by
  ext
  constructor
  · rintro ⟨f, rfl⟩
    simp only [cfcₙ_nnreal_eq_real f a]
    exact ⟨_, fun _ _ ↦ by positivity, rfl⟩
  · rintro ⟨f, hf, rfl⟩
    simp only [cfcₙ_real_eq_nnreal a hf]
    exact ⟨_, rfl⟩

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