English
If m(u) = ∞ whenever u has nonempty intersection with both s and t, then (boundedBy m)(s ∪ t) = (boundedBy m)(s) + (boundedBy m)(t).
Русский
Если m(u) = ∞ для любого множества u, у которого ненулевая пересечение с s и с t, то μ(s ∪ t) = μ(s) + μ(t) для μ = boundedBy m.
LaTeX
$$$\\forall s,t,\\ (\\forall u, (s \\cap u).Nonempty \\to (t \\cap u).Nonempty \\to m(u) = \\infty) \\Rightarrow \\mathrm{boundedBy}(m)(s \\cup t) = \\mathrm{boundedBy}(m)(s) + \\mathrm{boundedBy}(m)(t)$$$
Lean4
/-- If `m u = ∞` for any set `u` that has nonempty intersection both with `s` and `t`, then
`μ (s ∪ t) = μ s + μ t`, where `μ = MeasureTheory.OuterMeasure.boundedBy m`.
E.g., if `α` is an (e)metric space and `m u = ∞` on any set of diameter `≥ 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 boundedBy_union_of_top_of_nonempty_inter {s t : Set α}
(h : ∀ u, (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ∞) : boundedBy m (s ∪ t) = boundedBy m s + boundedBy m t :=
ofFunction_union_of_top_of_nonempty_inter fun u hs ht =>
top_unique <| (h u hs ht).ge.trans <| le_iSup (fun _ => m u) (hs.mono inter_subset_right)
