measurableSet_iInf — Mathlib

English

For a family m: ι → MeasurableSpace α, MeasurableSet[iInf m] s iff ∀ i, MeasurableSet[m i] s.

Русский

Для семейства $m_i$ множество измеримо в их iInf тогда и только тогда, когда измеримо в каждом $m_i$.

LaTeX

$$$\\text{MeasurableSet}[iInf m] s \\iff ∀ i, \\text{MeasurableSet}[m i] s$$$

Lean4

theorem measurableSet_iInf {ι} {m : ι → MeasurableSpace α} {s : Set α} :
    MeasurableSet[iInf m] s ↔ ∀ i, MeasurableSet[m i] s := by rw [iInf, measurableSet_sInf, forall_mem_range]

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