subsingleton

Mathlib.Logic.Equiv.Defs

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

English

If β is a Subsingleton type, then α ≃ β is a Subsingleton type; i.e., Subsingleton (α ≃ β).

Русский

Если β — пододномного типа, то α ≃ β является пододномным; то есть Subsingleton (α ≃ β).

LaTeX

$$$[Subsingleton \beta] \Rightarrow Subsingleton (\alpha \simeq \beta)$$$

Lean4

protected theorem subsingleton (e : α ≃ β) [Subsingleton β] : Subsingleton α :=
  e.injective.subsingleton

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

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

Разделы

Аффилиация

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