mem_measurableCylinders_of_mem_closedCompactCylinders

English

If two cylinders share the same index set, their intersection corresponds to the cylinder with the intersection of the base sets.

Русский

Если цилиндры имеют одинаковый набор индексов, их пересечение эквивалентно цилиндру с пересечением оснований.

LaTeX

$$$$\\mathrm{cylinder}(s,S_1) \\cap \\mathrm{cylinder}(s,S_2) = \\mathrm{cylinder}(s,S_1 \\cap S_2).$$$$

Lean4

theorem mem_measurableCylinders_of_mem_closedCompactCylinders [∀ i, MeasurableSpace (X i)]
    [∀ i, SecondCountableTopology (X i)] [∀ i, OpensMeasurableSpace (X i)] (ht : t ∈ closedCompactCylinders X) :
    t ∈ measurableCylinders X := by
  rw [mem_measurableCylinders]
  refine ⟨closedCompactCylinders.finset ht, closedCompactCylinders.set ht, ?_, ?_⟩
  · exact (closedCompactCylinders.isClosed ht).measurableSet
  · exact closedCompactCylinders.eq_cylinder ht

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