of_subsingleton — Mathlib

English

Let α be a subsingleton type and μ a measure on α. Then every subset s ⊆ α is NullMeasurable with respect to μ.

Русский

Пусть α представляет собой подсинглтонный тип и μ — меру на α. Тогда любое подмножество s ⊆ α является μ-нулеизмеримым.

LaTeX

$$$[Subsingleton\alpha] \Rightarrow \forall s \subseteq \alpha, \operatorname{NullMeasurableSet}(s,\mu)$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton α] : NullMeasurableSet s μ :=
  Subsingleton.measurableSet

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