Create a new file of bijectivity with all necessary lemmas.

New version of ae_op_compat is now proved using the previous result.

(includes bochner)

Function stuff moved to Function.v.
Some renaming.

(Some are still embryonic)

measurable_fun_swap.

Prove correctness results.

WIP: alternative def of is_topo_basis.

But need to keep both for one proof.