instDiscreteMeasurableSpace — Mathlib

English

There exists a discrete measurable space structure on α, in which every subset is measurable (provided suitable assumptions).

Русский

Существует дискретная σ‑алгебра на α, в которой каждое подмножество измеримо (при наличии соответствующих условий).

LaTeX

$$$\\exists \\mathcal{D} \\text{ on } \\alpha \\text{ such that } \\forall S\\subseteq\\alpha,\\ S \\in \\mathcal{D}.$$$

Lean4

instance : @DiscreteMeasurableSpace α ⊤ :=
  @DiscreteMeasurableSpace.mk _ (_) fun _ ↦ MeasurableSpace.measurableSet_top

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