measurableEmbedding_prod_mk_right

English

The map y ↦ (y, x) is a measurable embedding, using the standard prod map right-hand coordinate.

Русский

Отображение y ↦ (y, x) измеримо как вложение (правый координатный случай).

LaTeX

$$$\text{measurableEmbedding_prod_mk_right } (x) : \text{MeasurableEmbedding } (\lambda y, (y, x))$$$

Lean4

theorem measurableEmbedding_prod_mk_right [MeasurableSingletonClass α] (x : α) :
    MeasurableEmbedding (fun y ↦ (y, x) : β → β × α) :=
  MeasurableEmbedding.prodMk_right MeasurableEmbedding.id x

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