instIsStronglyCoatomicOfPredOrder

Mathlib.Order.Atoms

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

English

If α carries a PredOrder, then α is strongly coatomic.

Русский

Пусть на α задан предпорядок; тогда α является сильнокоатомной.

LaTeX

$$$\\mathrm{PredOrder}(\\alpha) \\Rightarrow \\mathrm{IsStronglyCoatomic}(\\alpha)$$$

Lean4

instance [PredOrder α] : IsStronglyCoatomic α := by rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; infer_instance

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

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

Разделы

Аффилиация

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