English
Let I = [0,1]. The map s: I → I defined by s(t) = 1 − t is a measure-preserving bijection with respect to the volume (Lebesgue) measure on I; equivalently, vol(S) = vol(s(S)) for every measurable S ⊆ I.
Русский
Пусть I = [0,1]. Отображение s: I → I, заданное s(t) = 1 − t, сохраняет меру на I; то есть для любого измеримого множества S ⊆ I выполняется vol(S) = vol(s(S)).
LaTeX
$$$\forall S \; (\text{Measurable}(S) \Rightarrow \operatorname{vol}(\{1 - x : x \in S\}) = \operatorname{vol}(S))$$$
Lean4
theorem measurePreserving_symm : MeasurePreserving symm volume volume
where
measurable := measurable_symm
map_eq := by
ext s hs
apply symmMeasurableEquiv.map_apply _ |>.trans
conv_lhs =>
rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm, ←
map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs), volume.measurePreserving_sub_left 1 |>.map_eq, ←
volume_apply]
