Commit 2024-11-19 08:43 8ad393d0
View on Github →feat(SetTheory/ZFC/Basic): results on pairs (#19144) We add a few lemmas on unordered pairs and use them to golf down the injectivity of the Kuratowski pair.
feat(SetTheory/ZFC/Basic): results on pairs (#19144) We add a few lemmas on unordered pairs and use them to golf down the injectivity of the Kuratowski pair.