lpMeasSubgroupToLpTrim_left_inv — Mathlib

English

The map lpMeasSubgroupToLpTrim is a left inverse of lpTrimToLpMeasSubgroup: composing lpMeasSubgroupToLpTrim after lpTrimToLpMeasSubgroup yields the original element.

Русский

Отображение lpMeasSubgroupToLpTrim является левым обратным к lpTrimToLpMeasSubgroup: композиция даёт исходный элемент.

LaTeX

$$$\text{LeftInverse}\bigl( lpTrimToLpMeasSubgroup\ F\ p\ μ\ hm\bigr)(\,lpMeasSubgroupToLpTrim\ F\ p\ μ\ hm\, f) = f$$$

Lean4

/-- `lpTrimToLpMeasSubgroup` is a left inverse of `lpMeasSubgroupToLpTrim`. -/
theorem lpMeasSubgroupToLpTrim_left_inv (hm : m ≤ m0) :
    Function.LeftInverse (lpTrimToLpMeasSubgroup F p μ hm) (lpMeasSubgroupToLpTrim F p μ hm) :=
  by
  intro f
  ext1
  ext1
  exact (lpTrimToLpMeasSubgroup_ae_eq hm _).trans (lpMeasSubgroupToLpTrim_ae_eq hm _)

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