isStronglyCoatomic_dual_iff_is_stronglyAtomic

English

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

Русский

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

LaTeX

$$$ IsStronglyCoatomic (OrderDual α) \iff IsStronglyAtomic α $$$

Lean4

@[simp]
theorem isStronglyCoatomic_dual_iff_is_stronglyAtomic : IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α := by
  rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]; rfl

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