map_iInf_le — Mathlib

English

For any function f: α → β and any family m_i of outer measures, map f applied to the infimum over i satisfies map f (⋂ m_i) ≤ ⋂ map f (m_i).

Русский

Для любой функции f: α → β и семейства внешних мер m_i справедливо: map f(inf_i m_i) ≤ inf_i map f(m_i).

LaTeX

$$$\\mathrm{map}_f(\\inf_i m_i) \\le \\inf_i \\mathrm{map}_f(m_i)$$$

Lean4

theorem map_iInf_le {ι β} (f : α → β) (m : ι → OuterMeasure α) : map f (⨅ i, m i) ≤ ⨅ i, map f (m i) :=
  (map_mono f).map_iInf_le

Похожие утверждения