chainClosure_maxChain

Mathlib.Order.CompleteLattice.Chain

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

English

The chain closure of r contains the maximal chain maxChain r.

Русский

Цепочная оболочка r содержит максимальную цепь maxChain r.

LaTeX

$$$ ChainClosure\, r\ (maxChain r) $$$

Lean4

theorem chainClosure_maxChain : ChainClosure r (maxChain r) :=
  ChainClosure.union fun _ => id

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

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

Разделы

Аффилиация

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