English
Restricting the ofFunction outer measure to a subset behaves as restricting the underlying m to intersections with that subset.
Русский
Ограничение внешней меры ofFunction до подмножества эквивалентно ограничению функции m на пересечения c этим подмножеством.
LaTeX
$$$\\mathrm{restrict\\_ofFunction} (s) (hm) :\\; \\mathrm{restrict}\\; s (\\text{OuterMeasure.ofFunction } m m\\_empty) = \\text{OuterMeasure.ofFunction } (\\lambda t. m (t \\cap s)) (by simp; simp [m\\_empty]).$$$
Lean4
theorem map_ofFunction {β} {f : α → β} (hf : Injective f) :
map f (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty :=
by
refine (map_ofFunction_le _).antisymm fun s => ?_
simp only [ofFunction_apply, map_apply, le_iInf_iff]
intro t ht
refine iInf_le_of_le (fun n => (range f)ᶜ ∪ f '' t n) (iInf_le_of_le ?_ ?_)
· rw [← union_iUnion, ← inter_subset, ← image_preimage_eq_inter_range, ← image_iUnion]
exact image_mono ht
· refine ENNReal.tsum_le_tsum fun n => le_of_eq ?_
simp [hf.preimage_image]
-- TODO (kmill): change `m (t ∩ s)` to `m (s ∩ t)`
