instIsStronglyAtomicOrderDualOfIsStronglyCoatomic

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#instIsStronglyAtomicOrderDualOfIsStronglyCoatomic

English

If α is strongly coatomic, then αᵒᵈ is strongly atomic.

Русский

Если α сильно коатомно, то αᵒᵈ сильно атомарно.

LaTeX

$$$ [IsStronglyCoatomic α] \Rightarrow IsStronglyAtomic (OrderDual α) $$$

Lean4

instance [IsStronglyCoatomic α] : IsStronglyAtomic αᵒᵈ := by rwa [isStronglyAtomic_dual_iff_is_stronglyCoatomic]

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

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

Разделы

Аффилиация

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