isChain

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#Set.Subsingleton.isChain

English

If s is a subsingleton, then s is a chain.

Русский

Если s — подмножество с не более чем одним элементом, то оно образует цепь.

LaTeX

$$$s \text{ SUBSINGLETON } \Rightarrow \operatorname{IsChain}(r,s)$$$

Lean4

theorem isChain (hs : s.Subsingleton) : IsChain r s :=
  hs.pairwise _

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

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

Разделы

Аффилиация

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