OAI/Combinatorics/TriangleRemoval/Embeddings/WitnessEmbeddingBound.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpTerminalLeave.WitnessEmbeddingBoundline 18 - lemma
OAI.SharpTerminalLeave.actual_witness_count_roots_eventuallyline 23 - theorem
OAI.SharpTerminalLeave.counted_traced_repeat_coverline 37 - instance
OAI.SharpTerminalLeave.instFintypeIndexedWitnessCodeEmbeddingBoundline 123