English
Let f be injective and let (m_i) be a family of outer measures on α. Then the pushforward along f distributes over the infimum via a restriction to the range of f: map_f(⨅_i m_i) = restrict(range(f))(⨅_i map_f(m_i)).
Русский
Пусть f инъективно и дано семейство внешних мер (m_i) на α. Тогда отображение вдоль f сохраняет инфимум, после ограничения к области значений f: map_f(⨅_i m_i) = restrict(range(f))(⨅_i map_f(m_i)).
LaTeX
$$$\operatorname{map}_f\left(\bigwedge_{i} m_i\right) = \operatorname{restrict}(\operatorname{range}(f))\left(\bigwedge_{i} \operatorname{map}_f(m_i)\right).$$$
Lean4
theorem map_iInf {ι β} {f : α → β} (hf : Injective f) (m : ι → OuterMeasure α) :
map f (⨅ i, m i) = restrict (range f) (⨅ i, map f (m i)) :=
by
refine Eq.trans ?_ (map_comap _ _)
simp only [comap_iInf, comap_map hf]
