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 _)