coe_measurableEquiv — Mathlib

English

The coercion of the measurableEquiv is equal to the canonical coordinate embedding; it is a simplification lemma.

Русский

Утверждается равенство коу-образования измеримой эквивалентности и канонического вложения координат; это лемма упрощения.

LaTeX

$$$(EuclideanSpace.measurableEquiv\,\iota).toFun = WithLp.ofLp$$$

Lean4

theorem coe_measurableEquiv : ⇑(EuclideanSpace.measurableEquiv ι) = WithLp.ofLp :=
  rfl

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