Theorem norm_cfc_lt

Modification history

2024-10-29 02:02
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
feat: lemma concerning for `‖cfc f a‖ < c` (#18361)
Added norm_cfc_ltView on Github →