mathlib3 documentation

measure_theory.function.strongly_measurable.inner

Inner products of strongly measurable functions are strongly measurable. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Strongly measurable functions #

@[protected]
@[protected]