Theorem Set.InvOn.one_sub_one_add_inv

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 Set.InvOn.one_sub_one_add_inv View on Github →