insert — Mathlib

English

If a set is null measurable with respect to μ, then inserting any point keeps it null measurable.

Русский

Если множество нулево измеримо по отношению к μ, добавление любой точки сохраняет нулевую измеримость.

LaTeX

$$$\\forall a, \\text{NullMeasurableSet } s μ \\Rightarrow \\text{NullMeasurableSet } (\\text{insert } a \\ s) μ$$$

Lean4

protected theorem insert [MeasurableSingletonClass (NullMeasurableSpace α μ)] (hs : NullMeasurableSet s μ) (a : α) :
    NullMeasurableSet (insert a s) μ :=
  MeasurableSet.insert hs a

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