OAI/Analysis/WeakInfiniteness/AnnihilatorStates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.realState_nonneg line 29
2. def OAI.WeakPureInfiniteness.annihilatorStates line 35
3. lemma OAI.WeakPureInfiniteness.annihilatorStates_isCompact line 39
4. lemma OAI.WeakPureInfiniteness.annihilatorStates_isExtreme line 55
5. lemma OAI.WeakPureInfiniteness.annihilatorStates_gns_zero line 70
6. theorem OAI.WeakPureInfiniteness.exists_extreme_annihilator_state line 88