Commit 2023-02-06 01:05 75d0ed47

View on Github →

feat: port Data.Setoid.Partition (#2066) port of data.setoid.partition mostly simple fixes. Commented out simp of mem_index to address simpNF

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Setoid/Partition.lean

added theorem Finpartition.isPartition_parts

added theorem IndexedPartition.class_of

added theorem IndexedPartition.disjoint

added theorem IndexedPartition.eq

added def IndexedPartition.equivQuotient

added theorem IndexedPartition.equivQuotient_index

added theorem IndexedPartition.equivQuotient_index_apply

added theorem IndexedPartition.equivQuotient_symm_proj_apply

added theorem IndexedPartition.exists_mem

added theorem IndexedPartition.index_out'

added theorem IndexedPartition.index_some

added theorem IndexedPartition.mem_iff_index_eq

added def IndexedPartition.out

added theorem IndexedPartition.out_proj

added def IndexedPartition.proj

added theorem IndexedPartition.proj_eq_iff

added theorem IndexedPartition.proj_fiber

added theorem IndexedPartition.proj_out

added theorem IndexedPartition.proj_some_index

added theorem IndexedPartition.some_index

added theorem IndexedPartition.unionᵢ

added structure IndexedPartition

added def Setoid.IsPartition.finpartition

added theorem Setoid.IsPartition.pairwiseDisjoint

added theorem Setoid.IsPartition.unionₛ_eq_univ

added def Setoid.IsPartition

added theorem Setoid.card_classes_ker_le

added def Setoid.classes

added theorem Setoid.classes_eqv_classes

added theorem Setoid.classes_inj

added theorem Setoid.classes_ker_subset_fiber_set

added theorem Setoid.classes_mkClasses

added theorem Setoid.empty_not_mem_classes

added theorem Setoid.eq_eqv_class_of_mem

added theorem Setoid.eq_iff_classes_eq

added theorem Setoid.eq_of_mem_classes

added theorem Setoid.eq_of_mem_eqv_class

added theorem Setoid.eqv_class_mem'

added theorem Setoid.eqv_class_mem

added theorem Setoid.eqv_classes_disjoint

added theorem Setoid.eqv_classes_of_disjoint_union

added theorem Setoid.exists_of_mem_partition

added theorem Setoid.finite_classes_ker

added theorem Setoid.isPartition_classes

added theorem Setoid.mem_classes

added def Setoid.mkClasses

added theorem Setoid.mkClasses_classes

added theorem Setoid.nonempty_of_mem_partition

added theorem Setoid.rel_iff_exists_classes

added def Setoid.setoidOfDisjointUnion

added theorem Setoid.unionₛ_classes