instMeasurableSingletonClass — Mathlib

English

If singleton sets are measurable in α and β, then every singleton in α × β is measurable; more precisely, { (a,b) } equals {a} × {b} and is measurable.

Русский

Если единичные множества измеримы в α и β, то каждый элемент пары имеет измеримое одинокое множество в α × β; то есть { (a,b) } = {a} × {b} и измеримо.

LaTeX

$$$\text{If }\operatorname{MeasurableSingletonClass}(\alpha)\ \text{and }\operatorname{MeasurableSingletonClass}(\beta),\text{ then } \operatorname{MeasurableSingletonClass}(\alpha \times \beta).$$$

Lean4

instance instMeasurableSingletonClass [MeasurableSingletonClass α] [MeasurableSingletonClass β] :
    MeasurableSingletonClass (α × β) :=
  ⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ .prod (.singleton a) (.singleton b)⟩

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