OAI/Analysis/Nuclearity/ClosedIdealImage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The closed image ideal of a surjective star homomorphism.

  1. def OAI.WeakPureInfiniteness.closedIdealImage line 15
  2. theorem OAI.WeakPureInfiniteness.mem_closedIdealImage line 46
  3. theorem OAI.WeakPureInfiniteness.functional_zero_on_closedIdealImage line 51