fundamentalFrontier — Mathlib

English

If s is a NullMeasurableSet with respect to a measure μ, then the fundamental frontier is also NullMeasurable with respect to μ.

Русский

Если s — нулемоизмеримое множество относительно меры μ, то и frontier является нулемоизмеримым множеством по отношению к μ.

LaTeX

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

Lean4

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

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