equiv_subsingleton_dom

Mathlib.Logic.Equiv.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

instance equiv_subsingleton_dom [Subsingleton α] : Subsingleton (α ≃ β) :=
  ⟨fun f _ => Equiv.ext fun _ => @Subsingleton.elim _ (Equiv.subsingleton.symm f) _ _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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