Commit 2021-12-07 18:28 a803e21d
View on Github →feat(measure_theory/lattice): define typeclasses for measurability of lattice operations, define a lattice on ae_eq_fun (#10591)
As was previously done for measurability of arithmetic operations, I define typeclasses for the measurability of sup and inf in a lattice. In the borel_space file, instances of these are provided when the lattice operations are continuous.
Finally I've put a lattice structure on ae_eq_fun.