Prove correctness results.

WIP: alternative def of is_topo_basis.

But need to keep both for one proof.

Add extensionality results on (pre)image.

WIP: being lazy with proofs of measurable_Rbar_abs and measurable_Rbar_scal.

Add missing proofs/results.