English
The map (x, f(y)) into α×β is a measurable embedding when f is a measurable embedding and x is fixed.
Русский
Отображение y ↦ (x, f(y)) является измеримым вложением, если f — измеримое вложение и фиксировано x.
LaTeX
$$$\text{prodMk_left } x \\text{ MeasurableEmbedding } f \Rightarrow \text{MeasurableEmbedding } (\lambda y, (x, f(y)))$$$
Lean4
/-- `Prod.map` of two measurable embeddings is a measurable embedding. -/
theorem prodMap {α β γ δ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
{mδ : MeasurableSpace δ} {f : α → β} {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
MeasurableEmbedding (Prod.map g f) :=
by
rw [MeasurableEmbedding.iff_comap_eq]
refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩
· rw [Prod.instMeasurableSpace, Prod.instMeasurableSpace, MeasurableSpace.comap_prodMap, hg.comap_eq, hf.comap_eq]
· rw [range_prodMap]
exact hg.measurableSet_range.prod hf.measurableSet_range
