English
If f is a homeomorphism of G to G and μ is preserved in the sense that μ(K.map f) = μ(K) for all compact K, then for any A ⊆ G we have μ.outerMeasure(f^{-1}(A)) = μ.outerMeasure(A).
Русский
Если f — гомеоморфизм G в G и μ сохраняется на компактных множествах K в виде μ(K.map f) = μ(K) для всех K, то для любого A ⊆ G выполняется μ.outerMeasure(f^{-1}(A)) = μ.outerMeasure(A).
LaTeX
$$$$\\forall A \\subset G:\\, μ.outerMeasure(f^{-1}(A)) = μ.outerMeasure(A)$$$$
Lean4
theorem outerMeasure_preimage (f : G ≃ₜ G) (h : ∀ ⦃K : Compacts G⦄, μ (K.map f f.continuous) = μ K) (A : Set G) :
μ.outerMeasure (f ⁻¹' A) = μ.outerMeasure A :=
by
refine inducedOuterMeasure_preimage _ μ.innerContent_iUnion_nat μ.innerContent_mono _ (fun _ => f.isOpen_preimage) ?_
intro s hs
convert μ.innerContent_comap f h ⟨s, hs⟩
