mathlib3

a803e21d - feat(measure_theory/lattice): define typeclasses for measurability of lattice operations, define a lattice on ae_eq_fun (#10591)

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`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>