isCoatomic_iff_forall_isCoatomic_Ici

English

In an order with a top, the poset is coatomic if and only if every Ici-interval is coatomic.

Русский

Если есть верхний элемент, то вся упорядоченность коатомна тогда и только тогда, когда каждый Ici-интервал коатомен.

LaTeX

$$$ IsCoatomic α \iff \forall x:α, IsCoatomic (Set.Ici x).Elem $$$

Lean4

theorem isCoatomic_iff_forall_isCoatomic_Ici [OrderTop α] : IsCoatomic α ↔ ∀ x : α, IsCoatomic (Set.Ici x) :=
  isAtomic_dual_iff_isCoatomic.symm.trans <|
    isAtomic_iff_forall_isAtomic_Iic.trans <| forall_congr' fun _ => isCoatomic_dual_iff_isAtomic.symm.trans Iff.rfl

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