measurableEquiv — Mathlib

English

The measurableEquiv between Euclidean space and the coordinate space has its coe equal to the canonical identification WithLp.ofLp.

Русский

Измеримая эквивалентность между Евклидовым пространством и координатным пространством имеет отображение-коэфициент, совпадающее с канонической идентификацией WithLp.ofLp.

LaTeX

$$$\mathrm{coe\;}\big(\mathrm{EuclideanSpace.measurableEquiv}) = \mathrm{WithLp.ofLp}$$$

Lean4

/-- `WithLp.equiv` as a `MeasurableEquiv`. -/
@[simps toEquiv]
protected def measurableEquiv : EuclideanSpace ℝ ι ≃ᵐ (ι → ℝ)
    where
  toEquiv := WithLp.equiv _ _
  measurable_toFun := measurable_id
  measurable_invFun := measurable_id

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