coe_symm_toMeasurableEquiv — Mathlib

English

The measurable equivalence of a map’s inverse equals the inverse measurable equivalence of the map.

Русский

Измеримое эквивалентность обращения отображения равна обращению измеримой эквивалентности самого отображения.

LaTeX

$$$f^{\\text{symm.toMeasurableEquiv}} = f^{\\text{toMeasurableEquiv}}^{\\text{symm}}$.$$

Lean4

@[simp]
theorem coe_symm_toMeasurableEquiv : ⇑f.toMeasurableEquiv.symm = f.symm :=
  rfl

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