feat: positive contractions in a C⋆-algebra form a directed set

[j-loreaux]

---

• depends on: [Merged by Bors] - feat: isometric continuous functional calculi #17837

[github-actions]

PR summary fc581b0291

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.CStarAlgebra.ApproximateUnit	2086

---

Declarations diff

+ CFC.monotoneOn_one_sub_one_add_inv
+ CStarAlgebra.directedOn_nonneg_ball
+ CStarAlgebra.le_nnnorm_of_mem_quasispectrum
+ Set.InvOn.one_sub_one_add_inv
+ Unitization.cfcₙ_eq_cfc_inr
+ Unitization.complex_cfcₙ_eq_cfc_inr
+ Unitization.real_cfcₙ_eq_cfc_inr
+ cfc_tsub
+ cfcₙ_tsub
+ nnnorm_cfc_lt
+ nnnorm_cfc_lt_iff
+ nnnorm_cfc_nnreal_lt
+ nnnorm_cfc_nnreal_lt_iff
+ nnnorm_cfcₙ_lt
+ nnnorm_cfcₙ_lt_iff
+ nnnorm_cfcₙ_nnreal_lt
+ nnnorm_cfcₙ_nnreal_lt_iff
+ nnreal_cfcₙ_eq_cfc_inr
+ norm_cfc_lt
+ norm_cfc_lt_iff
+ norm_cfcₙ_lt
+ norm_cfcₙ_lt_iff
+ norm_cfcₙ_one_sub_one_add_inv_lt_one
+ norm_def
+ quasispectrum_inr_eq
+ rpow_neg_one_eq_cfc_inv

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: isometric continuous functional calculi #17837
  By Dependent Issues (🤖). Happy coding!