lpMeasSubgroupToLpTrim_right_inv — Mathlib

English

The map lpTrimToLpMeasSubgroup is a right inverse of lpMeasSubgroupToLpTrim: applying lpTrimToLpMeasSubgroup after lpMeasSubgroupToLpTrim returns the original object.

Русский

Отображение lpTrimToLpMeasSubgroup является правым обратным к lpMeasSubgroupToLpTrim: после применения lpMeasSubgroupToLpTrim результат возвращает исходное объект.

LaTeX

$$$\text{RightInverse}\bigl(\,lpTrimToLpMeasSubgroup\ F\ p\ μ\ hm\bigr)\bigl(\,lpMeasSubgroupToLpTrim\ F\ p\ μ\ hm\bigr) = \mathrm{id}$$$

Lean4

/-- `lpTrimToLpMeasSubgroup` is a right inverse of `lpMeasSubgroupToLpTrim`. -/
theorem lpMeasSubgroupToLpTrim_right_inv (hm : m ≤ m0) :
    Function.RightInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm) :=
  by
  intro f
  ext1
  refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _) ?_
  exact (lpMeasSubgroupToLpTrim_ae_eq hm _).trans (lpTrimToLpMeasSubgroup_ae_eq hm _)

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