unique

Mathlib.Logic.Equiv.Defs

URI: https://scilib.ai/kg/mathlib#Equiv.unique

English

If α ≃ β and β is Unique, then α is Unique.

Русский

Если α ≃ β и β уникален, то и α уникален.

LaTeX

$$$\forall e:\alpha \simeq \beta, [Unique \beta] \Rightarrow Unique \alpha$$$

Lean4

/-- If `α ≃ β` and `β` is a singleton type, then so is `α`. -/
protected def unique [Unique β] (e : α ≃ β) : Unique α :=
  e.symm.surjective.unique

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru