OAI/Analysis/PureInfiniteness/ApproximateUnitConjugation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugation by a positive contractive approximate unit. This permits closed conjugation cones to recover their unconjugated generators even in a nonunital algebra.

  1. lemma OAI.WeakPureInfiniteness.approximateUnit_conjugation_tendsto line 16
  2. lemma OAI.WeakPureInfiniteness.continuous_functional_nonneg_of_conjugates line 36
  3. lemma OAI.WeakPureInfiniteness.isClosed_functional_conjugate_nonneg line 43