punitProd — Mathlib

English

There is a uniform isomorphism between PUnit × α and α, i.e., the unit component is irrelevant for the uniform structure.

Русский

Существует равномерное изоморфизм между PUnit × α и α, то есть единичный компонент не влияет на равномерную структуру.

LaTeX

$$$(PUnit \\times \\alpha) \\cong_{u} \\alpha$$$

Lean4

/-- `{*} × α` is uniformly isomorphic to `α`. -/
def punitProd : PUnit × α ≃ᵤ α :=
  (prodComm _ _).trans (prodPunit _)

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