prodPUnit — Mathlib

English

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

Русский

Правая единица: α × PUnit ≃ᵐ α.

LaTeX

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

Lean4

/-- `PUnit` is a right identity for product of measurable spaces up to a measurable equivalence. -/
def prodPUnit : α × PUnit ≃ᵐ α where
  toEquiv := Equiv.prodPUnit α
  measurable_toFun := measurable_fst
  measurable_invFun := measurable_prodMk_right

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