isChain_of_trichotomous

Mathlib.Order.Preorder.Chain

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

← MathLib Explorer

English

If the relation is trichotomous, any subset is a chain.

Русский

Если отношение тричотомично, любая подмножество является цепью.

LaTeX

$$[IsTrichotomous α r] (s ⊆ α) → IsChain r s$$

Lean4

theorem isChain_of_trichotomous [IsTrichotomous α r] (s : Set α) : IsChain r s := fun a _ b _ hab =>
  (trichotomous_of r a b).imp_right fun h => h.resolve_left hab

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

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

Разделы

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

Аффилиация

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