cfcₙ_nnreal — Mathlib

English

If a and b commute, then for any f: NNReal→NNReal, cfcₙ f a commutes with b.

Русский

Если a и b коммутируют, то для любого f: NNReal→NNReal, cfcₙ f a коммутирует с b.

LaTeX

$$$\\forall a,b\\in A\\; Commute(a,b) \\rightarrow \\forall f: NNReal \\to NNReal, Commute(cfcₙ f a, b)$$$

Lean4

/-- A version of `Commute.cfcₙ` or `IsSelfAdjoint.commute_cfcₙ` which does not require any
interaction with `star` when the base ring is `ℝ≥0`. -/
@[grind ←]
protected theorem cfcₙ_nnreal {a b : A} (hb : Commute a b) (f : ℝ≥0 → ℝ≥0) : Commute (cfcₙ f a) b :=
  by
  by_cases ha : 0 ≤ a
  · rw [cfcₙ_nnreal_eq_real ..]
    exact hb.cfcₙ_real _
  · simp [cfcₙ_apply_of_not_predicate a ha]

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