Theorem Function.extend_val_apply'

feat: if `g` is measurable wrt to the pullback by `f` then `g` is a measurable function of `f` (#22743) …