OAI/Computability/PerfectCompleteness/Machines/CanonicalLabelEncoding.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PerfectCompleteness.CanonicalLabelEncoding.labelIndexline 15 - def
OAI.PerfectCompleteness.CanonicalLabelEncoding.labelEmbeddingline 21 - theorem
OAI.PerfectCompleteness.CanonicalLabelEncoding.labelEmbedding_valline 25 - theorem
OAI.PerfectCompleteness.CanonicalLabelEncoding.labelIndex_eq_iffline 29 - def
OAI.PerfectCompleteness.CanonicalLabelEncoding.paddedMaskline 34 - theorem
OAI.PerfectCompleteness.CanonicalLabelEncoding.paddedMask_eq_true_iffline 37 - theorem
OAI.PerfectCompleteness.CanonicalLabelEncoding.label_card_leline 61 - theorem
OAI.PerfectCompleteness.CanonicalLabelEncoding.labelIndex_projectionline 66