of_comp_fst — Mathlib

English

If f is integrable with respect to μ×ν after composing with the first projection, then f is integrable with respect to μ provided ν ≠ 0.

Русский

Если f интегрируема по мере μ×ν после композиции с первой проекцией, то f интегрируема по μ при условии ν ≠ 0.

LaTeX

$$$\mathrm{Integrable}(f, μ×ν) \Rightarrow \mathrm{Integrable}(f, μ)$ under ν ≠ 0$$

Lean4

theorem of_comp_fst [SFinite μ] {f : α → E} (hf : Integrable (f ·.1) (μ.prod ν)) (hν : ν ≠ 0) : Integrable f μ :=
  hf.swap.of_comp_snd hν

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