lpTrimToLpMeasSubgroup — Mathlib

English

There is a natural map from lpMeas to Lp on μ.trim hm.

Русский

Существует естественное отображение lpMeas в Lp на μ.trim hm.

LaTeX

$$$\text{lpMeasToLpTrim}(hm, f) : Lp F p (μ.trim hm)$$$

Lean4

/-- Map from `Lp F p (μ.trim hm)` to `lpMeasSubgroup`, inverse of
`lpMeasSubgroupToLpTrim`. -/
noncomputable def lpTrimToLpMeasSubgroup (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) : lpMeasSubgroup F m p μ :=
  ⟨(memLp_of_memLp_trim hm (Lp.memLp f)).toLp f, mem_lpMeasSubgroup_toLp_of_trim hm f⟩

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