English
A preimage invariance under bijections that preserve P: the induced outer measure is invariant under taking preimages along an equivalence.
Русский
Инвариантность индуцированной внешней меры под предпобразованием вдоль эквивалентности, сохраняющей P.
LaTeX
$$Invariance of μ under preimage along f: inducedOuterMeasure m P0 m0 (f^{-1}(A)) = inducedOuterMeasure m P0 m0 A$$
Lean4
/-- If `P u` is `False` for any set `u` that has nonempty intersection both with `s` and `t`, then
`μ (s ∪ t) = μ s + μ t`, where `μ = inducedOuterMeasure m P0 m0`.
E.g., if `α` is an (e)metric space and `P u = diam u < r`, then this lemma implies that
`μ (s ∪ t) = μ s + μ t` on any two sets such that `r ≤ edist x y` for all `x ∈ s` and `y ∈ t`. -/
theorem inducedOuterMeasure_union_of_false_of_nonempty_inter {s t : Set α}
(h : ∀ u, (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u) :
inducedOuterMeasure m P0 m0 (s ∪ t) = inducedOuterMeasure m P0 m0 s + inducedOuterMeasure m P0 m0 t :=
ofFunction_union_of_top_of_nonempty_inter fun u hsu htu => @iInf_of_empty _ _ _ ⟨h u hsu htu⟩ _
