measurableSet — Mathlib

English

If α is a Subsingleton, then every subset s of α is measurable.

Русский

Если α является одиничным множеством, то любое подмножество s ⊆ α измеримо.

LaTeX

$$$[\text{Subsingleton } \alpha] \Rightarrow \forall s \subseteq \alpha,\ MeasurableSet(s)$$$

Lean4

@[nontriviality, measurability]
theorem measurableSet [Subsingleton α] {s : Set α} : MeasurableSet s :=
  Subsingleton.set_cases MeasurableSet.empty MeasurableSet.univ s

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