OAI/Analysis/WeakInfiniteness/InnerSubalgebras.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.IsClosedInner line 27
2. lemma OAI.WeakPureInfiniteness.hereditarySubalgebra_inner line 30
3. lemma OAI.WeakPureInfiniteness.hereditarySubalgebra_le_of_mem line 47
4. lemma OAI.WeakPureInfiniteness.IsClosedInner.symmetrized_corner_mem line 55