Sup` (#3185)

Commit

5 years ago

chore(measure_theory/outer_measure,measure_space): use `complete_lattice_of_Inf/Sup` (#3185) Also add a few supporting lemmas about `bsupr`/`binfi` to `order/complete_lattice`

Author

urkud

Parents

35fbfe0a

mathlib3 3d72c970 - chore(measure_theory/outer_measure,measure_space): use `complete_lattice_of_Inf/Sup` (#3185)

mathlib3
3d72c970 - chore(measure_theory/outer_measure,measure_space): use `complete_lattice_of_Inf/Sup` (#3185)