subperm_iff — Mathlib

English

For lists l1 and l2, l1 is a subpermutation of l2 if and only if there exists a list l such that l ~ l2 and l1 <+ l.

Русский

Для списков l1 и l2 верно: l1 <+~ l2 тогда и только тогда, когда существует список l, такой что l ~ l2 и l1 <+ l.

LaTeX

$$$l_1 <+~ l_2 \;\iff\; \exists l,\; l \sim l_2 \;\land\; l_1 <+ l$$$

Lean4

theorem subperm_iff : l₁ <+~ l₂ ↔ ∃ l, l ~ l₂ ∧ l₁ <+ l :=
  by
  refine ⟨?_, fun ⟨l, h₁, h₂⟩ ↦ h₂.subperm.trans h₁.subperm⟩
  rintro ⟨l, h₁, h₂⟩
  obtain ⟨l', h₂⟩ := h₂.exists_perm_append
  exact ⟨l₁ ++ l', (h₂.trans (h₁.append_right _)).symm, (prefix_append _ _).sublist⟩

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