cfc_nonneg_of_predicate — Mathlib

English

If a satisfies the predicate p and the function f is nonnegative on the spectrum of a, then cfc f a is nonnegative.

Русский

Если a удовлетворяет предикату p и f неотрицательно на спектре a, то cfc f a неотрицателен.

LaTeX

$$0 \le cfc f a \quad\text{whenever } (\forall x, x\in\mathrm{spectrum}\_R(a) \implies 0 \le f(x))$$

Lean4

@[simp]
theorem cfc_nonneg_of_predicate [LE A] [ContinuousFunctionalCalculus R A (0 ≤ ·)] {f : R → R} {a : A} : 0 ≤ cfc f a :=
  cfc_predicate _ _

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