OAI/Combinatorics/TriangleRemoval/Queries/AddressHead.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpTerminalLeave.PathForest.address_head line 21
2. lemma OAI.SharpTerminalLeave.PathForest.address_injective line 28
3. lemma OAI.SharpTerminalLeave.PathForest.prefix_address_mem line 34
4. lemma OAI.SharpTerminalLeave.PathForest.prefix_option_address_mem line 67
5. lemma OAI.SharpTerminalLeave.PathForest.two_mark_exact_size line 81
6. instance OAI.SharpTerminalLeave.indexedWitnessCodeAddressFintype line 114