mathlib

6f7c5394 - docs(order/complete_lattice): make two docstrings more detailed (#4859)

docs(order/complete_lattice): make two docstrings more detailed (#4859) Following [discussion](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Constructing.20a.20complete.20lattice), clarify information about how to construct a complete lattice while preserving good definitional equalities.