cfcHom_nonneg_iff — Mathlib

English

A simplified monotonicity variant for cfcHom under order relations.

Русский

Упрощённый вариант монотонности для cfcHom при отношении порядка.

LaTeX

$$cfcHom ha f ≤ cfcHom ha g$$

Lean4

theorem cfcHom_nonneg_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(spectrum R a, R)} :
    0 ≤ cfcHom ha f ↔ 0 ≤ f := by
  constructor
  · exact fun hf x ↦ (cfcHom_map_spectrum ha (R := R) _ ▸ spectrum_nonneg_of_nonneg hf) ⟨x, rfl⟩
  · simpa using (cfcHom_mono ha (f := 0) (g := f) ·)

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