comp_snd_iff — Mathlib

English

If μ is finite and ν ≠ 0, then Integrable (f ·.2) (μ×ν) is equivalent to Integrable f ν for f: α → E.

Русский

Если μ конечна и ν ≠ 0, то Integrable (f ·.2) (μ×ν) эквивалентно Integrable f ν для f: α → E.

LaTeX

$$$\mathrm{Integrable}(f\cdot\mathrm snd) (μ×ν) \iff \mathrm{Integrable}(f) ν$ under given finiteness assumptions$$

Lean4

theorem comp_snd_iff [IsFiniteMeasure μ] {f : β → E} (hμ : μ ≠ 0) : Integrable (f ·.2) (μ.prod ν) ↔ Integrable f ν :=
  ⟨(.of_comp_snd · hμ), (.comp_snd · μ)⟩

Похожие утверждения