feat(outer_measure): define bounded_by (#5314)
`bounded_by` wrapper around `of_function` that drops the condition that `m ∅ = 0`.
Refactor `Inf_gen` to use `bounded_by`.
I am also planning to use `bounded_by` for finitary products of measures.
Also add some complete lattice lemmas
