OAI/Combinatorics/RamseyFive/Trees/TreeDecoder.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.TreeCodec.decodedAt line 17
2. theorem OAI.SharpRamseyFive.TreeCodec.decodedAt_encoded line 29
3. theorem OAI.SharpRamseyFive.TreeCodec.observe_invariant line 43
4. lemma OAI.SharpRamseyFive.ReverseCap.cap_eviction_from_domination line 73
5. theorem OAI.SharpRamseyFive.ProjectiveIncidence.oriented_point_cap_eviction line 97
6. theorem OAI.SharpRamseyFive.ProjectiveIncidence.oriented_dual_cap_eviction line 126