Commit 2022-03-12 18:01 96bae07c

View on Github →

feat(order/complete_lattice): add complete_lattice.independent_pair (#12565) This makes complete_lattice.independent easier to work with in the degenerate case.

Estimated changes

Modified counterexamples/direct_sum_is_internal.lean

Modified src/data/set/basic.lean

added theorem set.insert_diff_eq_singleton

Modified src/order/complete_lattice.lean

added theorem complete_lattice.independent_pair

added theorem complete_lattice.set_independent_pair