equiv_subsingleton_cod

Mathlib.Logic.Equiv.Defs

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

English

If β is Subsingleton, then the type of equivalences α ≃ β is Subsingleton.

Русский

Если β — пододномный тип, то тип эквивалентностей α ≃ β пододном.

LaTeX

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

Lean4

instance equiv_subsingleton_cod [Subsingleton β] : Subsingleton (α ≃ β) :=
  ⟨fun _ _ => Equiv.ext fun _ => Subsingleton.elim _ _⟩

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

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

Разделы

Аффилиация

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