nullMeasurableSet

Mathlib.MeasureTheory.Measure.NullMeasurable

URI: https://scilib.ai/kg/mathlib#Set.Finite.nullMeasurableSet

English

If s is finite, then s is null-measurable with respect to μ.

Русский

Если s конечно множество, то оно является нулево измеримым относительно μ.

LaTeX

$$$s\text{ finite} \Rightarrow \mathrm{NullMeasurableSet}(s,\mu).$$$

Lean4

protected theorem _root_.Set.Finite.nullMeasurableSet (hs : s.Finite) : NullMeasurableSet s μ :=
  Finite.measurableSet hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru