measurableSet_sInf — Mathlib

English

The measurable sets of the infimum of a family of measurable spaces are those measurable in all members.

Русский

Пусть есть множество пространств измеримости; множество измеримо в infimum тогда и только тогда, когда измеримо во всех участниках.

LaTeX

$$$\\text{MeasurableSet}[m\\_inf] s \\iff ∀ m ∈ ms, \\text{MeasurableSet}[m] s$$$

Lean4

@[simp]
theorem measurableSet_sInf {ms : Set (MeasurableSpace α)} {s : Set α} :
    MeasurableSet[sInf ms] s ↔ ∀ m ∈ ms, MeasurableSet[m] s :=
  show s ∈ ⋂₀ _ ↔ _ by simp

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