Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-29 16:11 4cdfbd25

View on Github →

feat(data/setoid/partition): indexed partition (#7910) from LTE Note that data/setoid/partition.lean, which already existed before this PR, is currently not imported anywhere in mathlib. But it is used in LTE and will be used in the next PR, in relation to locally constant functions.

Estimated changes

Modified src/data/quot.lean

added theorem quotient.eq_mk_iff_out

added theorem quotient.mk_eq_iff_out

Modified src/data/setoid/basic.lean

modified theorem quotient.eq_rel

added theorem setoid.comap_rel

added theorem setoid.comm'

added theorem setoid.ker_apply_mk_out'

added theorem setoid.ker_apply_mk_out

Modified src/data/setoid/partition.lean

added theorem indexed_partition.Union

added theorem indexed_partition.class_of

added theorem indexed_partition.disjoint

added theorem indexed_partition.eq

added def indexed_partition.equiv_quotient

added theorem indexed_partition.equiv_quotient_index

added theorem indexed_partition.equiv_quotient_index_apply

added theorem indexed_partition.equiv_quotient_symm_proj_apply

added theorem indexed_partition.exists_mem

added theorem indexed_partition.index_out'

added theorem indexed_partition.index_some

added theorem indexed_partition.mem_iff_index_eq

added def indexed_partition.mk'

added def indexed_partition.out

added theorem indexed_partition.out_proj

added def indexed_partition.proj

added theorem indexed_partition.proj_eq_iff

added theorem indexed_partition.proj_fiber

added theorem indexed_partition.proj_out

added theorem indexed_partition.proj_some_index

added theorem indexed_partition.some_index

added structure indexed_partition

added theorem setoid.eqv_class_mem'