Commit 2024-04-24 14:51 2dac82fe

View on Github →

feat: ∃! x ∈ s, p x syntax (#12237) More generally, adds a binderPred variant for ExistsUnique. Uses this syntax to clean up Mathlib.Data.Setoid.Partition and remove Mathport warnings.

Estimated changes

modified def Setoid.IsPartition
modified theorem Setoid.classes_eqv_classes
modified theorem Setoid.classes_mkClasses
modified theorem Setoid.eq_eqv_class_of_mem
modified theorem Setoid.eq_of_mem_eqv_class
modified theorem Setoid.eqv_class_mem'
modified theorem Setoid.eqv_class_mem
modified theorem Setoid.eqv_classes_disjoint
modified def Setoid.mkClasses