punitProd — Mathlib

English

`PUnit` is a left identity for product of spaces up to a measurable equivalence: PUnit × α ≃ᵐ α.

Русский

Уравнение слева: PUnit является единицей слева для произведения пространств меры: PUnit × α ≃ᵐ α.

LaTeX

$$$ \text{punitProd}: PUnit \times \alpha \simeq^ᵐ \alpha $$$

Lean4

/-- `PUnit` is a left identity for product of measurable spaces up to a measurable equivalence. -/
def punitProd : PUnit × α ≃ᵐ α where
  toEquiv := Equiv.punitProd α
  measurable_toFun := measurable_snd
  measurable_invFun := measurable_prodMk_left

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