comp_fst_iff — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{Integrable}(f\cdot\mathrm fst) (μ×ν) \iff \mathrm{Integrable}(f) μ$ under σ-finite μ and ν ≠ 0$$

Lean4

theorem comp_fst_iff [SFinite μ] [IsFiniteMeasure ν] {f : α → E} (hν : ν ≠ 0) :
    Integrable (f ·.1) (μ.prod ν) ↔ Integrable f μ :=
  ⟨(.of_comp_fst · hν), (.comp_fst · ν)⟩

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