pair

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#IsChain.pair

English

If r a b holds, then {a,b} is a chain.

Русский

Если r a b выполняется, то множество {a,b} является цепью.

LaTeX

$$$\operatorname{IsChain}(r, \{a,b\})$$$

Lean4

theorem pair (h : r a b) : IsChain r { a, b } :=
  IsChain.singleton.insert fun _ hb _ ↦ .inl <| (eq_of_mem_singleton hb).symm.recOn ‹_›

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

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

Разделы

Аффилиация

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