def prodAssoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} : {x : MeasurableSpace α} → {x_1 : MeasurableSpace β} → {x_2 : MeasurableSpace γ} → (α × β) × γ ≃ᵐ α × β × γ

Canonical bijection between (α × β) × γ and α × β × γ.

Equations

• prodAssoc = { toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ }

def prodMKLeft_unit_equiv (α : Type u_4) [MeasurableSpace α] : Unit × α ≃ᵐ α

Measurable equivalence with the product with the one-point space Unit.

Equations

• prodMKLeft_unit_equiv α = { toEquiv := Equiv.punitProd α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem Measurable.of_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] {f : α → β} : Measurable f