subset_succChain

Mathlib.Order.Preorder.Chain

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

English

Every chain s is contained in its successor chain.

Русский

Каждая цепь s содержится в своей последующей цепи.

LaTeX

$$$\\\\forall \\\\alpha \\\\ r \\\\ s, s \\\\subseteq \\\\ SuccChain \\\\ r \\\\ s$$$

Lean4

theorem subset_succChain : s ⊆ SuccChain r s :=
  if h : ∃ t, IsChain r s ∧ SuperChain r s t then (succChain_spec h).2.1 else by simp [SuccChain, h]

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

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

Разделы

Аффилиация

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