instMeasurableSpace — Mathlib

English

Under a finite domain A, the MeasurableSpace on AddChar A M is the trivial measurable space.

Русский

При конечном множестве A и добавлении char, пространство измеримых множеств на AddChar A M тривиально.

LaTeX

$$$\mathrm{MeasurableSpace}(\mathrm{AddChar}\,A\,M) = \top$$$

Lean4

@[nolint unusedArguments]
instance instMeasurableSpace [DiscreteMeasurableSpace A] [Finite A] : MeasurableSpace (AddChar A M) :=
  ⊤

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