instIsAtomic

Mathlib.Order.Atoms

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

English

OrderDual α is atomic whenever α is coatomic.

Русский

Двойственный порядок αᵒᵈ атомарен тогда и только тогда, когда исходный порядок α коатомен.

LaTeX

$$$ IsCoatomic α \rightarrow IsAtomic (OrderDual α) $$$

Lean4

instance _root_.OrderDual.instIsAtomic : IsAtomic αᵒᵈ :=
  isAtomic_dual_iff_isCoatomic.2 ‹IsCoatomic α›

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

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

Разделы

Аффилиация

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