instMeasurableSpace

Mathlib.MeasureTheory.MeasurableSpace.Instances

URI: https://scilib.ai/kg/mathlib#ZMod.instMeasurableSpace

English

For every n, the measurable space on ZMod n is the top (indiscrete) one.

Русский

Для каждого n пространство измеримости на ZMod n является топовым.

LaTeX

$$$\operatorname{MeasurableSpace}(\mathbb{Z}/n\mathbb{Z}) = \top.$$$

Lean4

instance instMeasurableSpace (n : ℕ) : MeasurableSpace (ZMod n) :=
  ⊤

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

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

Разделы

Аффилиация

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