wellQuasiOrdered_of_isEmpty

Mathlib.Order.WellQuasiOrder

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

English

If the base type is empty, any relation is trivially a well-quasi-order.

Русский

Если множество пусто, любая связь тривиально является хорошим квазипорядком.

LaTeX

$$wellQuasiOrdered_of_isEmpty [IsEmpty α] (r : α → α → Prop) : WellQuasiOrdered r$$

Lean4

theorem wellQuasiOrdered_of_isEmpty [IsEmpty α] (r : α → α → Prop) : WellQuasiOrdered r := fun f ↦ isEmptyElim (f 0)

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

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

Разделы

Аффилиация

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