OAI/Probability/SignedSweeps/MarkedPairFibers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.markedSpinTransport_viaEmbedding_of_fixed line 12
2. def OAI.SignedSweeps.markedPairEmbeddingHom line 28
3. lemma OAI.SignedSweeps.pairEmbeddingHom_injective line 34
4. lemma OAI.SignedSweeps.markedPairEmbeddingHom_injective line 46
5. lemma OAI.SignedSweeps.markedPair_range_of_preserves line 52
6. def OAI.SignedSweeps.markedPairInsertion line 73
7. lemma OAI.SignedSweeps.inner_fiberInsertion line 78
8. lemma OAI.SignedSweeps.pairWord_inner_signed_off line 91
9. theorem OAI.SignedSweeps.markedPairInsertion_off line 112