isCoatomic_of_orderTop_gt_wellFounded

English

If α has a top element and WellFoundedGT holds, then α is coatomic.

Русский

Если у α есть верхняя граница и WellFoundedGT выполняется, то α коатомна.

LaTeX

$$$\\left[OrderTop(\\alpha)\\right] \\land \\mathrm{WellFounded}((>)) \\Rightarrow \\mathrm{IsCoatomic}(\\alpha)$$$

Lean4

theorem isCoatomic_of_orderTop_gt_wellFounded [OrderTop α] (h : WellFounded ((· > ·) : α → α → Prop)) : IsCoatomic α :=
  isAtomic_dual_iff_isCoatomic.1 (@isAtomic_of_orderBot_wellFounded_lt αᵒᵈ _ _ h)

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