OAI/Analysis/PureInfiniteness/OneStepContraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The one-step case of Kirchberg--Rørdam (2002), Lemma 7.2. Approximate inner implementations of a contractive map can be chosen contractive, including in a nonunital algebra.

  1. lemma OAI.WeakPureInfiniteness.exists_positive_contraction_sandwich_approximation line 16
  2. lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepInner.contractive_implementations line 44