OAI/Analysis/Nuclearity/IdealSeparatingRepresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A closed ideal and an element outside it are separated by an actual irreducible representation. This is the first representation step of Tomiyama's product-state separation argument.

  1. theorem OAI.WeakPureInfiniteness.exists_pure_state_gns_detecting line 20
  2. theorem OAI.WeakPureInfiniteness.exists_ideal_separating_irreducible line 37