OAI/Analysis/Nuclearity/IdealInIdeal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A closed ideal in a C*-ideal is an ideal in the containing algebra. The proof uses the approximate unit of the smaller ideal.

  1. def OAI.WeakPureInfiniteness.idealImageHom line 17
  2. theorem OAI.WeakPureInfiniteness.RightIdealRange.idealImage line 21
  3. def OAI.WeakPureInfiniteness.idealInIdealImage line 38
  4. theorem OAI.WeakPureInfiniteness.mem_idealInIdealImage line 52