OAI/Analysis/WeakInfiniteness/FaithfulRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.sumRepresentation line 33
2. lemma OAI.WeakPureInfiniteness.sumRepresentation_apply line 57
3. lemma OAI.WeakPureInfiniteness.sumRepresentation_injective line 60
4. def OAI.WeakPureInfiniteness.universalGNSHilbert line 79
5. def OAI.WeakPureInfiniteness.universalGNSRepresentation line 82
6. lemma OAI.WeakPureInfiniteness.universalGNSRepresentation_injective line 86
7. theorem OAI.WeakPureInfiniteness.exists_faithful_representation line 100