fundamentalInterior — Mathlib

English

If s is a NullMeasurableSet with respect to μ, then the fundamental interior is NullMeasurable with respect to μ.

Русский

Если s — нулемоизмеримое множество относительно μ, то fundamentalInterior(G,s) также нулемоизмеримо.

LaTeX

$$NullMeasurableSet(s, μ) ⇒ NullMeasurableSet(fundamentalInterior(G,s), μ)$$

Lean4

@[to_additive MeasureTheory.NullMeasurableSet.addFundamentalInterior]
protected theorem fundamentalInterior (hs : NullMeasurableSet s μ) : NullMeasurableSet (fundamentalInterior G s) μ :=
  hs.diff <| .iUnion fun _ => .iUnion fun _ => hs.smul _

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