SuperChain

Mathlib.Order.Preorder.Chain

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

English

SuperChain(s,t) means that t is a chain that strictly includes s.

Русский

SuperChain(s,t) означает, что t является цепью и строго содержит s.

LaTeX

$$$\operatorname{SuperChain}(s,t) \equiv \operatorname{IsChain}(r,t) \land s \subsetneq t$$$

Lean4

/-- `SuperChain s t` means that `t` is a chain that strictly includes `s`. -/
def SuperChain (s t : Set α) : Prop :=
  IsChain r t ∧ s ⊂ t

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

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

Разделы

Аффилиация

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