swap — Mathlib

English

If f is IntegrableOn on s×t, then the swapped function is IntegrableOn on t×s with respect to ν.prod μ.

Русский

Если f интегрируемо на s×t, тогда переставленная функция интегрируема на t×s по ν×μ.

LaTeX

$$$\mathrm{IntegrableOn}(f, s×t, μ×ν) \Rightarrow \mathrm{IntegrableOn}(f\circ\mathrm{Prod.swap}, t×s, ν×μ)$$$

Lean4

theorem swap [SFinite μ] {f : α × β → E} {s : Set α} {t : Set β} (hf : IntegrableOn f (s ×ˢ t) (μ.prod ν)) :
    IntegrableOn (f ∘ Prod.swap) (t ×ˢ s) (ν.prod μ) :=
  by
  rw [IntegrableOn, ← Measure.prod_restrict] at hf ⊢
  exact hf.swap

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