prodUnique — Mathlib

English

If β is a Unique type, then α × β ≃ α; i.e., β contributes no information to the product.

Русский

Если β уникальный тип, то α × β ≃ α; то есть β не несет дополнительной информации в произведении.

LaTeX

$$$$ \\alpha \\times \\beta \\simeq \\alpha \\quad\\text{when } \\beta \\text{ is unique}. $$$$

Lean4

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

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