instNonempty

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#OrderDual.instNonempty

English

If α is nonempty, then its order dual αᵒᵈ is also nonempty.

Русский

Если α непусто, то его дуальный порядок αᵒᵈ тоже непуст.

LaTeX

$$$ \forall \alpha,\; \text{Nonempty}(\alpha) \Rightarrow \text{Nonempty}(\alpha^{\mathrm{op}}) $$$

Lean4

instance (α : Type*) [h : Nonempty α] : Nonempty αᵒᵈ :=
  h

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

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

Разделы

Аффилиация

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