isStronglyAtomic_dual_iff_is_stronglyCoatomic

English

IsStronglyAtomic on the dual order is equivalent to IsStronglyCoatomic on the original order.

Русский

Сильная атомарность двойственного порядка эквивалентна сильной коатомности исходного порядка.

LaTeX

$$$ IsStronglyAtomic α^{\mathrm{op}} \iff IsStronglyCoatomic α $$$

Lean4

theorem isStronglyAtomic_dual_iff_is_stronglyCoatomic : IsStronglyAtomic αᵒᵈ ↔ IsStronglyCoatomic α := by
  simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall, OrderDual.toDual_le_toDual, and_comm,
    isStronglyCoatomic_iff] using forall_comm

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