OAI/Analysis/WeakInfiniteness/CentralVacuum.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.fockVacuum line 29
  2. lemma OAI.WeakPureInfiniteness.fockVacuum_norm line 31
  3. def OAI.WeakPureInfiniteness.oInfinityVacuumState line 34
  4. lemma OAI.WeakPureInfiniteness.oInfinityVacuumState_one line 37
  5. lemma OAI.WeakPureInfiniteness.oInfinityVacuumState_isometry line 43
  6. def OAI.WeakPureInfiniteness.oInfinityCentralStateMap line 47
  7. lemma OAI.WeakPureInfiniteness.oInfinityCentralStateMap_apply line 51
  8. lemma OAI.WeakPureInfiniteness.oInfinityCentralStateMap_cp line 56
  9. lemma OAI.WeakPureInfiniteness.oInfinityCentralStateMap_norm_le line 62
  10. lemma OAI.WeakPureInfiniteness.exists_unital_cpc_central_map_killing_generators line 71