Commit 2022-03-11 08:22 47b1ddf2

View on Github →

feat(data/setoid/partition): Relate setoid.is_partition and finpartition (#12459) Add two functions that relate setoid.is_partition and finpartition:

setoid.is_partition.partition
finpartition.is_partition_parts Meanwhile add some lemmas related to finset.sup and finset.inf in data/finset/lattice.

Estimated changes

Modified src/data/finset/lattice.lean

added theorem finset.inf_id_set_eq_sInter

added theorem finset.inf_set_eq_bInter

added theorem finset.sup_id_set_eq_sUnion

added theorem finset.sup_set_eq_bUnion

Modified src/data/setoid/partition.lean

added theorem finpartition.is_partition_parts

added def setoid.is_partition.finpartition

Modified src/order/well_founded_set.lean