Lattice operations on encodable types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Lemmas about lattice and set operations on encodable types
Implementation Notes #
This is a separate file, to avoid unnecessary imports in basic files.
Previously some of these results were in the