Commit 2021-12-15 19:58 02cdc812

View on Github →

refactor(order/sup_indep): Get rid of decidable equality assumption (#10673) The erase in the definition required a decidable_eq. We can make do without it while keeping it functionally the same.

Estimated changes

Modified src/order/sup_indep.lean

modified theorem complete_lattice.independent_iff_sup_indep

modified theorem finset.sup_indep.bUnion

modified theorem finset.sup_indep.pairwise_disjoint

modified theorem finset.sup_indep.sup

modified def finset.sup_indep

modified theorem finset.sup_indep_empty

added theorem finset.sup_indep_iff_disjoint_erase

modified theorem finset.sup_indep_iff_pairwise_disjoint