Theorem nnnorm_cfcₙ_nnreal_lt_iff

Modification history

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