instMeasurableSingletonClass — Mathlib

English

In the natural numbers with its standard measurable space, every singleton {n} is measurable.

Русский

В натуральных числах, снабжённых стандартной структурой измеримости, для каждого n множество {n} является измеримым.

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, \\, MeasurableSet(\\\\{n\\\\})$$$

Lean4

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

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