instMeasurableSingletonClass

Mathlib.MeasureTheory.MeasurableSpace.Instances

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

English

In the integers ℤ with its canonical measurable structure, every singleton {k} is measurable.

Русский

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

LaTeX

$$$\\\\forall k \\\\in \\\\mathbb{Z}, \\\\ MeasurableSet(\\\\{k\\\\})$$$

Lean4

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

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

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

Разделы

Аффилиация

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