Commit 2025-03-19 12:24 4aa8b04d

View on Github →

refactor(Logic/Equiv/List): split (#23092) The motivation here is to delay the import of sorting.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Countable.lean

Modified Mathlib/Logic/Encodable/Pi.lean

Created Mathlib/Logic/Equiv/Finset.lean

added def Denumerable.lower'

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 theorem Denumerable.raise_lower'

added def Encodable.fintypeEquivFin

added theorem Encodable.length_sortedUniv

added theorem Encodable.mem_sortedUniv

added def Encodable.sortedUniv

added theorem Encodable.sortedUniv_nodup

added theorem Encodable.sortedUniv_toFinset

Modified Mathlib/Logic/Equiv/List.lean

deleted def Denumerable.lower'

deleted def Denumerable.lower

deleted theorem Denumerable.lower_raise'

deleted theorem Denumerable.lower_raise

deleted def Denumerable.raise'

deleted def Denumerable.raise'Finset

deleted theorem Denumerable.raise'_chain

deleted theorem Denumerable.raise'_sorted

deleted def Denumerable.raise

deleted theorem Denumerable.raise_chain

deleted theorem Denumerable.raise_lower'

deleted theorem Denumerable.raise_lower

deleted theorem Denumerable.raise_sorted

deleted def Encodable.decodeMultiset

deleted def Encodable.encodeMultiset

deleted def Encodable.fintypeEquivFin

deleted theorem Encodable.length_sortedUniv

deleted theorem Encodable.mem_sortedUniv

deleted def Encodable.sortedUniv

deleted theorem Encodable.sortedUniv_nodup

deleted theorem Encodable.sortedUniv_toFinset

Created Mathlib/Logic/Equiv/Multiset.lean

added def Denumerable.lower

added theorem Denumerable.lower_raise

added def Denumerable.raise

added theorem Denumerable.raise_chain

added theorem Denumerable.raise_lower

added theorem Denumerable.raise_sorted

added def decodeMultiset

added def encodeMultiset

Modified Mathlib/ModelTheory/Order.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean