nullMeasurableSet — Mathlib

English

A convex set in a finite-dimensional real vector space is null measurable with respect to an additive Haar measure.

Русский

В конечномерном вещественном пространстве выпуклое множество нулево замеряемо по аддитивной мере Хаара.

LaTeX

$$$\\text{NullMeasurableSet}(s, \\mu)$ для $s$ выпукло и $\mu$-мера Хаара.$$

Lean4

/-- A convex set in a finite-dimensional real vector space is null measurable with respect to an
additive Haar measure on this space. -/
protected theorem nullMeasurableSet (hs : Convex ℝ s) : NullMeasurableSet s μ :=
  nullMeasurableSet_of_null_frontier (hs.addHaar_frontier μ)

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