instIsStronglyCoatomicOfWellFoundedGT

Mathlib.Order.Atoms

URI: https://scilib.ai/kg/mathlib#instIsStronglyCoatomicOfWellFoundedGT

English

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

Русский

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

LaTeX

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

Lean4

instance [WellFoundedGT α] : IsStronglyCoatomic α :=
  IsStronglyCoatomic.of_wellFounded_gt wellFounded_gt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru