punitEquivPUnit — Mathlib

English

Two universes carry equivalent PUnit sorts; there is a natural equivalence PUnit_v ≃ PUnit_w with toFun and invFun both sending unit to unit.

Русский

Сорта PUnit в разных вселенных взаимно эквивалентны; существует естественная эквивалентность PUnit_v ≃ PUnit_w с мерами toFun и invFun, отправляющими единицу в единицу.

LaTeX

$$$ PUnit_{v} \simeq PUnit_{w} $$$

Lean4

/-- `PUnit` sorts in any two universes are equivalent. -/
def punitEquivPUnit : PUnit.{v} ≃ PUnit.{w} where
  toFun _ := .unit
  invFun _ := .unit

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