integrable_inv_smul_measure — Mathlib

English

If c ≠ 0 and c ≠ ∞, Integrable f (c⁻¹•μ) ↔ Integrable f μ.

Русский

Если c ≠ 0 и c ≠ ∞, Integrable(f, c⁻¹ μ) эквивалентно Integrable(f, μ).

LaTeX

$$Integrable f (c⁻¹ • μ) ↔ Integrable f μ, for c ≠ 0, ∞.$$

Lean4

theorem integrable_inv_smul_measure {f : α → ε} {c : ℝ≥0∞} (h₁ : c ≠ 0) (h₂ : c ≠ ∞) :
    Integrable f (c⁻¹ • μ) ↔ Integrable f μ :=
  integrable_smul_measure (by simpa using h₂) (by simpa using h₁)

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