empty_mem_measurableCylinders — Mathlib

English

The empty set is a member of the measurable cylinders collection.

Русский

Пустое множество входит в множество измеримых цилиндров.

LaTeX

$$$ \\emptyset \\in \\mathrm{measurableCylinders}(\\alpha) $$$

Lean4

theorem empty_mem_measurableCylinders (α : ι → Type*) [∀ i, MeasurableSpace (α i)] : ∅ ∈ measurableCylinders α :=
  by
  simp_rw [measurableCylinders, mem_iUnion, mem_singleton_iff]
  exact ⟨∅, ∅, MeasurableSet.empty, (cylinder_empty _).symm⟩

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