Commit 2024-08-11 23:33 e5667e51
View on Github →feat(Integral): lemma about integrating a function X → C(Y, E) (#15627)
Given a function f : X → C(Y, E), we have that (∫ x, f x ∂μ) y = ∫ x, f x y ∂μ.
feat(Integral): lemma about integrating a function X → C(Y, E) (#15627)
Given a function f : X → C(Y, E), we have that (∫ x, f x ∂μ) y = ∫ x, f x y ∂μ.