Commit 2024-10-30 16:54 e15c6ebb

View on Github →

feat: positive contractions in a C⋆-algebra form a directed set (#18016)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

added theorem CFC.monotoneOn_one_sub_one_add_inv

added theorem CStarAlgebra.directedOn_nonneg_ball

added theorem Set.InvOn.one_sub_one_add_inv

added theorem norm_cfcₙ_one_sub_one_add_inv_lt_one

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

added theorem CStarAlgebra.le_nnnorm_of_mem_quasispectrum

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean

added theorem CFC.rpow_neg_one_eq_cfc_inv

Modified Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean

added theorem ContinuousMapZero.norm_def