mem_measurableCylinders — Mathlib

English

For a set t, t is in measurableCylinders if and only if there exist a finite index set s and a base S with MeasurableSet S such that t = cylinder s S.

Русский

Для множества t существует конечное множество индексов s и основание S, измеримое, такое что t = cylinder s S, если и только если t принадлежит измеримым цилиндрам.

LaTeX

$$$ t \\in \\mathrm{measurableCylinders}(\\alpha) \\iff \\exists s,S,\\mathrm{MeasurableSet}(S) \\land t = \\mathrm{cylinder}(s,S) $$$

Lean4

@[simp]
theorem mem_measurableCylinders (t : Set (∀ i, α i)) :
    t ∈ measurableCylinders α ↔ ∃ s S, MeasurableSet S ∧ t = cylinder s S := by
  simp_rw [measurableCylinders, mem_iUnion, exists_prop, mem_singleton_iff]

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