Theorem norm_cfcₙ_one_sub_one_add_inv_lt_one

Modification history

2024-10-30 16:54
Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean
feat: positive contractions in a C⋆-algebra form a directed set (#18016)
Added norm_cfcₙ_one_sub_one_add_inv_lt_oneView on Github →