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]