integrableOn_iff — Mathlib

English

For hs, ht, and invariant f, IntegrableOn f on s is equivalent to IntegrableOn f on t.

Русский

Для hs, ht и инвариантной f выполняется эквивалентность IntegrableOn на s и на t.

LaTeX

$$$$\\text{IntegrableOn}(f, s, \\mu) \\iff \\text{IntegrableOn}(f, t, \\mu).$$$$

Lean4

@[to_additive]
protected theorem integrableOn_iff (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → E}
    (hf : ∀ (g : G) (x), f (g • x) = f x) : IntegrableOn f s μ ↔ IntegrableOn f t μ :=
  and_congr (hs.aestronglyMeasurable_on_iff ht hf) (hs.hasFiniteIntegral_on_iff ht hf)

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