measurableEmbedding_prodMk_left — Mathlib

English

Similarly, the map y ↦ (f(y), x) is a measurable embedding when f is a measurable embedding.

Русский

Аналогично отображение y ↦ (f(y), x) является измеримым вложением, если f — измеримое вложение.

LaTeX

$$$\text{prodMk_right } (hf)\; (x) : \text{MeasurableEmbedding } (\lambda y, (f(y), x))$$$

Lean4

theorem measurableEmbedding_prodMk_left [MeasurableSingletonClass α] (x : α) :
    MeasurableEmbedding (Prod.mk x : β → α × β) :=
  MeasurableEmbedding.prodMk_left x MeasurableEmbedding.id

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