infix

Mathlib.Data.List.Chain

URI: https://scilib.ai/kg/mathlib#List.IsChain.infix

Lean4

theorem «infix» (h : IsChain R l) (h' : l₁ <:+: l) : IsChain R l₁ :=
  by
  rcases h' with ⟨l₂, l₃, rfl⟩
  exact h.left_of_append.right_of_append

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

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

Разделы

Аффилиация

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