OAI/Combinatorics/SharpRamsey/Geometry/ProjectiveTransport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLogRamsey.ProjectiveDuality.incident_mapEquiv line 15
2. lemma OAI.SharpLogRamsey.ProjectiveDuality.incidenceCount_mapEquiv line 27
3. lemma OAI.SharpLogRamsey.ProjectiveDuality.incidenceCount_bidual line 40
4. lemma OAI.SharpLogRamsey.ProjectiveDuality.pullback_cover line 49