coe_toEquiv — Mathlib

English

For any equivalence e: α ≃ β with measurable and inverse measurable, the measurable equivalence built from e coincides with e when viewed as a function.

Русский

Для всякого эквивалента e: α ≃ β, который измерим и обратимый измерим, эквивалентность MeasurableEquiv, построенная из e, совпадает с e как функцией.

LaTeX

$$$$ ((\langle e, h_1, h_2 \rangle : \alpha \simeq_m \beta) : \alpha \to \beta) = e. $$$$

Lean4

@[simp]
theorem coe_toEquiv (e : α ≃ᵐ β) : (e.toEquiv : α → β) = e :=
  rfl

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