OAI/Analysis/JiangSu/Excision/PureGNSStrongDensity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PureStateExcision.scalar_entries_commute line 20
2. lemma OAI.PureStateExcision.strong_density_of_scalar_commutant line 36
3. theorem OAI.PureStateExcision.pure_gns_strong_approximation line 62
4. def OAI.PureStateExcision.selfAdjointOrbit line 90
5. lemma OAI.PureStateExcision.selfadjoint_strong_density_of_scalar_commutant line 99
6. theorem OAI.PureStateExcision.pure_gns_selfadjoint_strong_approximation line 139
7. lemma OAI.PureStateExcision.symmetric_rankTwo_maps line 166
8. lemma OAI.PureStateExcision.pure_state_small_left_error line 177