infix_antisymm

Mathlib.Data.List.Infix

URI: https://scilib.ai/kg/mathlib#List.infix_antisymm

English

If l1 is an infix of l2 and l2 is an infix of l1, then l1 = l2.

Русский

Если l1 является инфиксом l2 и наоборот, то списки равны.

LaTeX

$$$\forall {l_1 l_2 : \text{List}(\alpha)},\; l_1 <:+: l_2 \wedge l_2 <:+: l_1 \Rightarrow l_1 = l_2.$$$

Lean4

theorem infix_antisymm {l₁ l₂ : List α} (h₁ : l₁ <:+: l₂) (h₂ : l₂ <:+: l₁) : l₁ = l₂ :=
  h₁.sublist.antisymm h₂.sublist

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

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

Разделы

Аффилиация

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