English
Let f: α → β be a function and let (m_i) be a family of outer measures on β. Then taking the comap along f commutes with arbitrary infima: comap_f(⨅_i m_i) = ⨅_i comap_f(m_i).
Русский
Пусть f: α → β и семейство внешних мер (m_i) на β. Тогда взятие предобраза по f и инфимума по i приводят к одному результату: comap_f(⨅_i m_i) = ⨅_i comap_f(m_i).
LaTeX
$$$\operatorname{comap}_f\left(\bigwedge_{i} m_i\right) = \bigwedge_{i} \operatorname{comap}_f(m_i).$$$
Lean4
theorem comap_iInf {ι β} (f : α → β) (m : ι → OuterMeasure β) : comap f (⨅ i, m i) = ⨅ i, comap f (m i) :=
by
refine ext_nonempty fun s hs => ?_
refine ((comap_mono f).map_iInf_le s).antisymm ?_
simp only [comap_apply, iInf_apply' _ hs, iInf_apply' _ (hs.image _), le_iInf_iff, Set.image_subset_iff,
preimage_iUnion]
refine fun t ht => iInf_le_of_le _ (iInf_le_of_le ht <| ENNReal.tsum_le_tsum fun k => ?_)
exact iInf_mono fun i => (m i).mono (image_preimage_subset _ _)
