instUniqueOfIsEmpty

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.instUniqueOfIsEmpty

English

If α is empty, then there is a unique Sublattice of α; implemented as an instance.

Русский

Если α пусто, существует единственная подрешетка α; оформлено как экземпляр.

LaTeX

$$IsEmpty α ⇒ Unique (Sublattice α)$$

Lean4

instance [IsEmpty α] : Unique (Sublattice α) where uniq _ := @Subsingleton.elim _ (subsingleton_iff.2 ‹_›) _ _

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

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

Разделы

Аффилиация

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