sigmaPUnit — Mathlib

English

Dependent product with PUnit is equivalent to the base type: (α) × PUnit ≃ α.

Русский

Зависимое произведение с PUnit эквивалентно базовому типу: (α) × PUnit ≃ α.

LaTeX

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

Lean4

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

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