wellFoundedGT_iff_isSupFiniteCompact

Mathlib.Order.CompactlyGenerated.Basic

URI: https://scilib.ai/kg/mathlib#CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact

English

WellFoundedGT α is equivalent to IsSupFiniteCompact α.

Русский

WellFoundedGT α эквивалентно IsSupFiniteCompact α.

LaTeX

$$WellFoundedGT α ↔ IsSupFiniteCompact α$$

Lean4

theorem wellFoundedGT_iff_isSupFiniteCompact : WellFoundedGT α ↔ IsSupFiniteCompact α :=
  (wellFoundedGT_characterisations α).out 0 1

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

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

Разделы

Аффилиация

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