Commit 2020-07-15 16:50 5fe67b77

feat(measure_theory): preliminaries for Haar measure (#3195) Move properties about lattice operations on encodable types to a new file. These are generalized from lemmas in the measure theory folder, for lattice operations and not just for ennreal. Also move them to the encodable namespace. Rename outer_measure.Union_aux to encodable.Union_decode2. Generalize some properties for outer measures to arbitrary complete lattices. This is useful for operations that behave like outer measures on a subset of set α.