Commit 2024-09-11 03:54 e992840b

View on Github →

chore: move ExistsUnique, Xor' out of Init.Logic (#16691) As well as deprecate another unused lemma.

Estimated changes

deleted theorem ExistsUnique.elim
deleted theorem ExistsUnique.exists
deleted theorem ExistsUnique.intro
deleted theorem ExistsUnique.unique
deleted def ExistsUnique
deleted def Xor'
deleted theorem existsUnique_congr
deleted theorem ExistsUnique.elim₂
deleted theorem ExistsUnique.exists₂
deleted theorem ExistsUnique.intro₂
deleted theorem ExistsUnique.unique₂
added def Xor'
deleted theorem exists_unique_const
deleted theorem exists_unique_eq'
deleted theorem exists_unique_eq
deleted theorem exists_unique_false
deleted theorem exists_unique_iff_exists
deleted theorem exists_unique_prop
added theorem ExistsUnique.elim
added theorem ExistsUnique.elim₂
added theorem ExistsUnique.exists
added theorem ExistsUnique.exists₂
added theorem ExistsUnique.intro
added theorem ExistsUnique.intro₂
added theorem ExistsUnique.unique
added theorem ExistsUnique.unique₂
added def ExistsUnique
added theorem existsUnique_congr
added theorem exists_unique_const
added theorem exists_unique_eq'
added theorem exists_unique_eq
added theorem exists_unique_false
added theorem exists_unique_prop