not_superChain

Mathlib.Order.Preorder.Chain

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

English

A maximal chain cannot be strictly extended by a SuperChain.

Русский

Максимальная цепь не может быть строго расширена суперкцепью.

LaTeX

$$$ IsMaxChain\\ r\\ s \\rightarrow \\neg\\operatorname{SuperChain}\\ r\\ s\\ t $$$

Lean4

theorem not_superChain (h : IsMaxChain r s) : ¬SuperChain r s t := fun ht => ht.2.ne <| h.2 ht.1 ht.2.1

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

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

Разделы

Аффилиация

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