Commit 2023-04-12 19:26 da5ce5ae

View on Github →

feat: port Computability.Encoding (#2799)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/Encoding.lean

added theorem Computability.Encoding.card_le_aleph0

added theorem Computability.Encoding.card_le_card_list

added theorem Computability.Encoding.encode_injective

added structure Computability.Encoding

added theorem Computability.FinEncoding.card_le_aleph0

added structure Computability.FinEncoding

added def Computability.decodeBool

added def Computability.decodeNat

added def Computability.decodeNum

added def Computability.decodePosNum

added theorem Computability.decode_encodeBool

added theorem Computability.decode_encodeNat

added theorem Computability.decode_encodeNum

added theorem Computability.decode_encodePosNum

added def Computability.encodeBool

added def Computability.encodeNat

added def Computability.encodeNum

added def Computability.encodePosNum

added theorem Computability.encodePosNum_nonempty

added def Computability.encodingNatBool

added def Computability.encodingNatΓ'

added def Computability.finEncodingBoolBool

added def Computability.finEncodingNatBool

added def Computability.finEncodingNatΓ'

added def Computability.inclusionBoolΓ'

added theorem Computability.inclusionBoolΓ'_injective

added theorem Computability.leftInverse_section_inclusion

added def Computability.sectionΓ'Bool

added def Computability.unaryDecodeNat

added def Computability.unaryEncodeNat

added def Computability.unaryFinEncodingNat

added theorem Computability.unary_decode_encode_nat

added inductive Computability.Γ'