iSup' — Mathlib

English

Mapping commutes with arbitrary suprema: map distributes over iSup.

Русский

Отображение распределяется по верхней сумме: map f над iSup равен iSup над map f.

LaTeX

$$$$ \mathrm{map}\, f \bigl( \bigvee_i m_i \bigr) = \bigvee_i \bigl( \mathrm{map}\, f (m_i) \bigr) $$$$

Lean4

theorem iSup' {mα : ι → MeasurableSpace α} {_ : MeasurableSpace β} {f : α → β} (i₀ : ι) (h : Measurable[mα i₀] f) :
    Measurable[⨆ i, mα i] f :=
  h.mono (le_iSup mα i₀) le_rfl

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