English
The inverse of a measurable equivalence is the measurable equivalence of the inverse map.
Русский
Обратная измеримая эквивалентность равна измеримой эквивалентности обратной карты.
LaTeX
$$$(f^{\\text{toMeasurableEquiv}})^{-1} = (f^{-1})^{\\text{toMeasurableEquiv}}$.$$
Lean4
/-- The volume form coming from an orientation in an inner product space gives measure `1` to the
parallelepiped associated to any orthonormal basis. This is a rephrasing of
`abs_volumeForm_apply_of_orthonormal` in terms of measures. -/
theorem measure_orthonormalBasis (o : Orientation ℝ F (Fin n)) (b : OrthonormalBasis ι ℝ F) :
o.volumeForm.measure (parallelepiped b) = 1 :=
by
have e : ι ≃ Fin n := by
refine Fintype.equivFinOfCardEq ?_
rw [← _i.out, finrank_eq_card_basis b.toBasis]
have A : ⇑b = b.reindex e ∘ e := by
ext x
simp only [OrthonormalBasis.coe_reindex, Function.comp_apply, Equiv.symm_apply_apply]
rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped, o.abs_volumeForm_apply_of_orthonormal,
ENNReal.ofReal_one]
