coe_measurableEquiv_symm — Mathlib

English

The inverse of the measurableEquiv is the standard lifting to WithLp; the symmetry holds at the level of functions.

Русский

Обратная к измеримой эквивалентности имеет стандартное поднятие до WithLp; симметрия сохраняется на уровне функций.

LaTeX

$$$(EuclideanSpace.measurableEquiv\,\iota)^{-1} = WithLp.toLp$$$

Lean4

theorem coe_measurableEquiv_symm : ⇑(EuclideanSpace.measurableEquiv ι).symm = WithLp.toLp _ :=
  rfl

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