isChain

Mathlib.Order.Preorder.Chain

URI: https://scilib.ai/kg/mathlib#IsMaxChain.isChain

English

A maximal chain is a chain.

Русский

Максимальная цепь является цепью.

LaTeX

$$$ IsMaxChain\\ r\\ s \\rightarrow IsChain\\ r\\ s $$$

Lean4

theorem isChain (h : IsMaxChain r s) : IsChain r s :=
  h.1

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

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

Разделы

Аффилиация

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