uniqueProd — Mathlib

English

If β is unique, then β × α ≃ α; this is a left-identity variant of the previous fact.

Русский

Если β уникальный, то β × α ≃ α; это лево-идентичность предыдущего факта.

LaTeX

$$$$ \\beta \\times \\alpha \\simeq \\alpha \\quad\\text{when } [Unique\\ \\beta]. $$$$

Lean4

/-- Any `Unique` type is a left identity for type product up to equivalence. -/
def uniqueProd (α β) [Unique β] : β × α ≃ α :=
  ((equivPUnit.{_, 1} β).prodCongr <| Equiv.refl α).trans <| punitProd α

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