_ge_0 _empty -> _nonneg
_False -> _emptyset

Use emptyset and nonneg.

*_seq'* -> *_seq_Rbar*

measurable_fun _ gen_Rbar -> measurable_fun_Rbar _.
Move stuff on restricted measure into measure.v.
Add lemma meas_prod_is_tensor_product_measure.

measure.is_sigma_finite_measure_equiv_def.

- add bijectivity in mu2_restricted_sigma_additivity lemma.
- create a new record of measure restricted.