English
For any indexing ι and f: α → β, the pushforward along f commutes with taking the infimum of comapped outer measures: map_f(⨅_i comap_f(m_i)) = ⨅_i map_f(comap_f(m_i)).
Русский
Пусть индексы i∈ι и функция f задают отображение, тогда отображение вдоль f commute с инфимумом от предобразованных мер: map_f(⨅_i comap_f(m_i)) = ⨅_i map_f(comap_f(m_i)).
LaTeX
$$$\operatorname{map}_f\left(\bigwedge_{i} \operatorname{comap}_f(m_i)\right) = \bigwedge_{i} \operatorname{map}_f\bigl(\operatorname{comap}_f(m_i)\bigr).$$$
Lean4
theorem map_iInf_comap {ι β} [Nonempty ι] {f : α → β} (m : ι → OuterMeasure β) :
map f (⨅ i, comap f (m i)) = ⨅ i, map f (comap f (m i)) :=
by
refine (map_iInf_le _ _).antisymm fun s => ?_
simp only [map_apply, comap_apply, iInf_apply, le_iInf_iff]
refine fun t ht => iInf_le_of_le (fun n => f '' t n ∪ (range f)ᶜ) (iInf_le_of_le ?_ ?_)
· rw [← iUnion_union, Set.union_comm, ← inter_subset, ← image_iUnion, ← image_preimage_eq_inter_range]
exact image_mono ht
· refine ENNReal.tsum_le_tsum fun n => iInf_mono fun i => (m i).mono ?_
simpa only [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty, image_subset_iff] using
subset_rfl
