OAI/Analysis/JiangSu/Excision/PureGNSProjections.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PureStateExcision.projection_vector_value line 17
2. lemma OAI.PureStateExcision.projection_vector_sum line 26
3. lemma OAI.PureStateExcision.commuting_operator_eq_zero_of_cyclic line 37
4. theorem OAI.PureStateExcision.pure_gns_commutant_projection line 51
5. lemma OAI.PureStateExcision.invariant_starProjection_commute line 140
6. theorem OAI.PureStateExcision.pure_gns_invariant_subspace line 153
7. def OAI.PureStateExcision.orbitLinear line 172
8. lemma OAI.PureStateExcision.orbit_invariant line 177
9. theorem OAI.PureStateExcision.pure_gns_nonzero_cyclic line 184