Commit 2023-01-20 10:06 3af1cb32

View on Github →

feat: port Logic.Equiv.List (#1709)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Countable/Defs.lean

Created Mathlib/Logic/Equiv/List.lean

added theorem Denumerable.denumerable_list_aux

added theorem Denumerable.list_ofNat_succ

added theorem Denumerable.list_ofNat_zero

added def Denumerable.lower'

added def Denumerable.lower

added theorem Denumerable.lower_raise'

added theorem Denumerable.lower_raise

added def Denumerable.raise'

added def Denumerable.raise'Finset

added theorem Denumerable.raise'_chain

added theorem Denumerable.raise'_sorted

added def Denumerable.raise

added theorem Denumerable.raise_chain

added theorem Denumerable.raise_lower'

added theorem Denumerable.raise_lower

added theorem Denumerable.raise_sorted

added def Encodable.decodeList

added def Encodable.decodeMultiset

added theorem Encodable.decode_list_succ

added theorem Encodable.decode_list_zero

added def Encodable.encodableOfList

added def Encodable.encodeList

added def Encodable.encodeMultiset

added theorem Encodable.encode_list_cons

added theorem Encodable.encode_list_nil

added def Encodable.fintypeArrow

added def Encodable.fintypeEquivFin

added def Encodable.fintypePi

added theorem Encodable.length_le_encode

added theorem Encodable.length_sortedUniv

added theorem Encodable.mem_sortedUniv

added def Encodable.sortedUniv

added theorem Encodable.sortedUniv_nodup

added theorem Encodable.sortedUniv_toFinset

added def Equiv.listEquivSelfOfEquivNat

added def Equiv.listNatEquivNat

added def Equiv.listUnitEquiv

added def Fintype.truncEncodable