English
If s and t are in measurable cylinders, then their intersection s ∩ t is also in measurable cylinders.
Русский
Если оба множества принадлежат измеримым цилиндрам, их пересечение тоже принадлежит измеримым цилиндрам.
LaTeX
$$$ \\text{If } s,t \\in \\mathrm{measurableCylinders}(\\alpha), \\; s \\cap t \\in \\mathrm{measurableCylinders}(\\alpha). $$$
Lean4
theorem inter_mem_measurableCylinders (hs : s ∈ measurableCylinders α) (ht : t ∈ measurableCylinders α) :
s ∩ t ∈ measurableCylinders α := by
rw [mem_measurableCylinders] at *
obtain ⟨s₁, S₁, hS₁, rfl⟩ := hs
obtain ⟨s₂, S₂, hS₂, rfl⟩ := ht
classical
refine
⟨s₁ ∪ s₂,
Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩ {f | Finset.restrict₂ Finset.subset_union_right f ∈ S₂}, ?_,
?_⟩
· refine MeasurableSet.inter ?_ ?_
· exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₁
· exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _) hS₂
· exact inter_cylinder _ _ _ _
