map_biInf_comap — Mathlib

English

Let I be a nonempty set of indices. For f: α → β and a family m_i of outer measures on β, the map of the infimum over i∈I of comap_f(m_i) equals the infimum over i∈I of map_f(comap_f(m_i)).

Русский

Пусть I непустое множество индексов. Тогда отображение вдоль f и инфимум по i∈I от предобразов согласуются: map_f(⨅_{i∈I} comap_f(m_i)) = ⨅_{i∈I} map_f(comap_f(m_i)).

LaTeX

$$$\operatorname{map}_f\left(\bigwedge_{i\in I} \operatorname{comap}_f(m_i)\right) = \bigwedge_{i\in I} \operatorname{map}_f\bigl(\operatorname{comap}_f(m_i)\bigr).$$$

Lean4

theorem map_biInf_comap {ι β} {I : Set ι} (hI : I.Nonempty) {f : α → β} (m : ι → OuterMeasure β) :
    map f (⨅ i ∈ I, comap f (m i)) = ⨅ i ∈ I, map f (comap f (m i)) :=
  by
  haveI := hI.to_subtype
  rw [← iInf_subtype'', ← iInf_subtype'']
  exact map_iInf_comap _

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