Theorem: Measure_theory.L2.integrable_mul (Untitled/Probability/Indep.lean)

State before:
α : Type u_1
m1 m2 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
hm : m1 ≤ m2
⊢ ∀ (f g : ↥(Lp ℝ 2)), Integrable fun x => ↑↑f x * ↑↑g x
Tactic:
apply L2.integrable_inner
State after:
no goals