prodMk_right — Mathlib

English

The map y ↦ (f(y), x) is a measurable embedding for any x, given f is a measurable embedding.

Русский

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

LaTeX

$$$\forall x, \text{MeasurableEmbedding } (\lambda y, (f(y), x))$$$

Lean4

theorem prodMk_right {β γ : Type*} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
    {f : γ → β} (hf : MeasurableEmbedding f) (x : α) : MeasurableEmbedding (fun y ↦ (f y, x)) :=
  MeasurableEquiv.prodComm.measurableEmbedding.comp (hf.prodMk_left _)

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