English
There exists a measurable embedding y ↦ (x, f(y)) with injectivity and measurability properties when f is a measurable embedding.
Русский
Существует измеримое вложение y ↦ (x, f(y)) с инъективностью и измеримостными свойствами при f — измеримое вложение.
LaTeX
$$$\text{prodMk_left } x \;\text{(hf : MeasurableEmbedding f)} \Rightarrow \text{MeasurableEmbedding } (\lambda y, \langle x, f(y)\rangle)$$$
Lean4
theorem prodMk_left {β γ : Type*} [MeasurableSingletonClass α] {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (x : α)
{f : γ → β} (hf : MeasurableEmbedding f) : MeasurableEmbedding (fun y ↦ (x, f y))
where
injective := by
intro y y'
simp only [Prod.mk.injEq, true_and]
exact fun h ↦ hf.injective h
measurable := Measurable.prodMk measurable_const hf.measurable
measurableSet_image' := by
intro s hs
convert (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)
ext x
simp [Prod.ext_iff, eq_comm, ← exists_and_left, and_left_comm]
