measurableSet_inf — Mathlib

English

The measurable sets of the infimum of a family of sigma-algebras are exactly those that are measurable in every member of the family.

Русский

Множество измеримо в infimum (пересечении) сигма-алгебр тогда и только когда измеримо в каждой из них.

LaTeX

$$$\\text{MeasurableSet}[m_\\inf] s \\iff \\forall m \\in ms, \\ MeasurableSet[m] s$$$

Lean4

@[simp]
  -- The `m₁` parameter gets filled in by typeclass instance synthesis (for some reason...)
  -- so we have to order it *after* `m₂`. Otherwise `simp` can't apply this lemma.

theorem measurableSet_inf {m₂ m₁ : MeasurableSpace α} {s : Set α} :
    MeasurableSet[m₁ ⊓ m₂] s ↔ MeasurableSet[m₁] s ∧ MeasurableSet[m₂] s :=
  Iff.rfl

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