instSubsingleton — Mathlib

English

If the underlying space is subsingleton, then the associated null-measurable space is subsingleton.

Русский

Если пространство тождественно однородно (subs) — то соответствующее пространство нулевой измеримости также тождественно однородно.

LaTeX

$$$$ \\text{Subsingleton}(\\text{NullMeasurableSpace} \\, \\alpha \\, \\mu) $$$$

Lean4

instance instSubsingleton [h : Subsingleton α] : Subsingleton (NullMeasurableSpace α μ) :=
  h

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