instIsStronglyCoatomic — Mathlib

English

If α is a preordered set, then αᵒᵈ is strongly coatomic whenever α is strongly atomic.

Русский

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

LaTeX

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

Lean4

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

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