finite_of_isAntichain

Mathlib.Order.WellQuasiOrder

URI: https://scilib.ai/kg/mathlib#WellQuasiOrderedLE.finite_of_isAntichain

← MathLib Explorer

English

In a WellQuasiOrderedLE α, every antichain with respect to ≤ is finite.

Русский

В WellQuasiOrderedLE α каждая антицепь относительно ≤ конечна.

LaTeX

$$$[WellQuasiOrderedLE\\;\\alpha]\\ {s:Set\\alpha},\\ IsAntichain(\\le, s)\\Rightarrow s.Finite$$$

Lean4

theorem finite_of_isAntichain [WellQuasiOrderedLE α] {s : Set α} (h : IsAntichain (· ≤ ·) s) : s.Finite :=
  h.finite_of_wellQuasiOrdered wellQuasiOrdered_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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