instMeasurableSingletonClass

Mathlib.MeasureTheory.MeasurableSpace.Instances

URI: https://scilib.ai/kg/mathlib#Rat.instMeasurableSingletonClass

English

In the rationals ℚ with its standard measurable structure, every singleton {q} is measurable.

Русский

В рациональных числах ℚ с обычной структурой измеримости каждое множество {q} измеримо.

LaTeX

$$$\\\\forall q \\\\in \\\\mathbb{Q}, \\\\ MeasurableSet(\\\\{q\\\\})$$$

Lean4

instance instMeasurableSingletonClass : MeasurableSingletonClass ℚ :=
  ⟨fun _ => trivial⟩

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

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

Разделы

Аффилиация

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