comap_iSup — Mathlib

English

For f : α → β and m_i OuterMeasure β, comap f (⨆ i, m_i) = ⨆ i, comap f (m_i).

Русский

Для f : α → β и внешних мер m_i на β выполняется comap f (⨆ i, m_i) = ⨆ i, comap f (m_i).

LaTeX

$$$ comap\ f\ (\bigsup_{i} m_i) = \bigsup_{i} (comap\ f\ (m_i)) $$$

Lean4

@[simp]
theorem comap_iSup {β ι} (f : α → β) (m : ι → OuterMeasure β) : comap f (⨆ i, m i) = ⨆ i, comap f (m i) :=
  ext fun s => by simp only [comap_apply, iSup_apply]

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