of_wellFounded_gt — Mathlib

English

If WellFounded_gt on α holds, then α is strongly coatomic.

Русский

Если gt на α является хорошо основанным, тогда α сильнокоатомна.

LaTeX

$$$\\mathrm{WellFounded}((>)) \\Rightarrow \\mathrm{IsStronglyCoAtomic}(\\alpha)$$$

Lean4

theorem of_wellFounded_gt (h : WellFounded ((· > ·) : α → α → Prop)) : IsStronglyCoatomic α :=
  isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| IsStronglyAtomic.of_wellFounded_lt (α := αᵒᵈ) h

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