OAI/Analysis/IrrationalRotation/Product/ProductPairSanity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.cocycleRatio_self line 12
2. theorem OAI.Invariant233.ProductModel.ratioDiagonal_self line 16
3. theorem OAI.Invariant233.ProductModel.pairIdentity_self_iff line 29
4. theorem OAI.Invariant233.ProductModel.triangularLaw_empty_eq_diagonal line 37
5. theorem OAI.Invariant233.ProductModel.measurableEmbedding_diagonalPair line 52
6. theorem OAI.Invariant233.ProductModel.triangularLaw_empty_ae_iff line 68
7. theorem OAI.Invariant233.ProductModel.triangularLaw_empty_pairIdentity_iff line 73