isAtomic_of_orderBot_wellFounded_lt

English

If α has a bottom element and LT is well-founded, then α is atomic.

Русский

Если на α имеется минимум и LT хорошо основано, то α атомарна.

LaTeX

$$$\\mathrm{OrderBot}(\\alpha) \\land \\mathrm{WellFounded}((<)) \\Rightarrow \\mathrm{IsAtomic}(\\alpha)$$$

Lean4

theorem isAtomic_of_orderBot_wellFounded_lt [OrderBot α] (h : WellFounded ((· < ·) : α → α → Prop)) : IsAtomic α :=
  (IsStronglyAtomic.of_wellFounded_lt h).isAtomic

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