OAI/SetTheory/PartitionPrinciple/Definability/CodedBatchDecoding.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.decodeline 16 - theorem
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encode_decodeline 19 - theorem
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.decode_encodeline 22 - def
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encodingIsoline 25 - def
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.decodingIsoline 29 - theorem
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encodingIso_valueline 32 - theorem
OAI.PartitionPilot.Forcing.CodedTemplateAttachment.decodingIso_encodeline 35