instNoAtomsElemRealVolume

Mathlib.MeasureTheory.Constructions.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.instNoAtomsElemRealVolume

English

The unit interval volume has no atoms: every singleton has measure zero.

Русский

У единичного интервала мера объёма не имеет точечных атомов: любому одиночному элементу соответствует нулевой объём.

LaTeX

$$$\forall x\in I:\, \operatorname{volume}({x}) = 0$$$

Lean4

instance : NoAtoms (volume : Measure I) where measure_singleton x := by simp [volume_apply]

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

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

Разделы

Аффилиация

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