univ_mem_measurableCylinders — Mathlib

English

The universal set is a member of measurableCylinders α.

Русский

Общее множество является членом множества измеримых цилиндров.

LaTeX

$$$ \\mathrm{Set.univ} \\in \\mathrm{measurableCylinders}(\\alpha). $$$

Lean4

theorem univ_mem_measurableCylinders (α : ι → Type*) [∀ i, MeasurableSpace (α i)] : Set.univ ∈ measurableCylinders α :=
  by rw [← compl_empty]; exact compl_mem_measurableCylinders (empty_mem_measurableCylinders α)

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