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]