isWF_univ_iff

Mathlib.Order.WellFoundedSet

URI: https://scilib.ai/kg/mathlib#Set.isWF_univ_iff

English

For LT α, IsWF(univ) is equivalent to WellFoundedLT α.

Русский

Для LT α IsWF(универсум) эквивалентно WellFoundedLT α.

LaTeX

$$IsWF(univ) \\iff WellFoundedLT α$$

Lean4

theorem isWF_univ_iff : IsWF (univ : Set α) ↔ WellFoundedLT α := by simp [IsWF, wellFoundedOn_iff, isWellFounded_iff]

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

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

Разделы

Аффилиация

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