prodPUnit — Mathlib

English

PUnit acts as a right identity for type products up to equivalence: α × PUnit ≃ α.

Русский

PUnit служит правым тождественным элементом для декартова произведения типов: α × PUnit ≃ α.

LaTeX

$$$$ \\alpha \\times \\mathrm{PUnit} \\simeq \\alpha. $$$$

Lean4

/-- `PUnit` is a right identity for type product up to an equivalence. -/
@[simps (attr := grind =)]
def prodPUnit (α) : α × PUnit ≃ α where
  toFun := fun p => p.1
  invFun := fun a => (a, PUnit.unit)

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