mathlib
96bae07c - feat(order/complete_lattice): add `complete_lattice.independent_pair` (#12565)

Commit

3 years ago

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

Author

eric-wieser

Parents

7e5ac6ad

mathlib 96bae07c - feat(order/complete_lattice): add `complete_lattice.independent_pair` (#12565)

mathlib
96bae07c - feat(order/complete_lattice): add `complete_lattice.independent_pair` (#12565)