integrable_comp_iff — Mathlib

English

If φ is integrable and L is a continuous linear equivalence, then φ mapped by L is integrable and vice versa.

Русский

Если φ интегрируемо и L — непрерывное линейное эквивалентное отображение, то φ и L(φ) интегрируемы взаимно.

LaTeX

$$$ \\operatorname{Integrable}(\\phi,\\mu) \\Rightarrow \\operatorname{Integrable}(x \\mapsto L(\\phi(x)),\\mu) $$$

Lean4

@[simp]
theorem integrable_comp_iff {φ : α → H} (L : H ≃ₛₗᵢ[σ] E) : Integrable (fun a : α ↦ L (φ a)) μ ↔ Integrable φ μ :=
  ContinuousLinearEquiv.integrable_comp_iff (L : H ≃SL[σ] E)

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