Theorems · Theorem · measure theory

MeasurableEmbedding.prodMk_left

∀ {α : Type u_1} [inst : MeasurableSpace α] {β : Type u_3} {γ : Type u_4} [MeasurableSingletonClass α]
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (x : α) {f : γ → β},
  MeasurableEmbedding f → MeasurableEmbedding fun y => (x, f y)

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Prod

Cited by

2 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSingletonClass