instDiscreteMeasurableSpace — Mathlib

English

In the extended naturals ℕ∞ with its canonical measurable structure, every singleton {x} is measurable.

Русский

В расширенных натуральных числах ℕ∞ с канонической структурой измеримости каждое множество-одиночка {x} измеримо.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{N}_\\\\infty, \\\\ MeasurableSet(\\\\{x\\\\})$$$

Lean4

instance instDiscreteMeasurableSpace : DiscreteMeasurableSpace ℕ∞ :=
  ⟨fun _ ↦ trivial⟩

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