OAI/Combinatorics/Progressions/Linear/SplitCoverProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.sublatticeProjection line 15
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.sublatticeProjection_mk line 18
3. theorem OAI.Erdos3.RationalFilteredNilmanifold.sublatticeProjection_surjective line 21
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.sublatticeProjection_lipschitz line 29
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.sublattice_pullback_lipschitz line 49
6. def OAI.Erdos3.RationalFilteredNilmanifold.splitCoverProjection line 74
7. theorem OAI.Erdos3.RationalFilteredNilmanifold.splitCoverProjection_surjective line 78
8. theorem OAI.Erdos3.RationalFilteredNilmanifold.splitCoverProjection_mk line 81
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.splitCoverProjection_lipschitz line 96
10. theorem OAI.Erdos3.RationalFilteredNilmanifold.splitCoverProjection_pullback line 109