sym2 — Mathlib

English

If xs ~ ys then xs.sym2 ~ ys.sym2.

Русский

Если xs ~ ys, тогда xs.sym2 ~ ys.sym2.

LaTeX

$$$$ xs.Perm ys \\Rightarrow xs.sym2.Perm ys.sym2 $$$$

Lean4

protected theorem sym2 {xs ys : List α} (h : xs <+ ys) : xs.sym2 <+ ys.sym2 := by
  induction h with
  | slnil => apply slnil
  | cons a h ih =>
    simp only [List.sym2]
    exact Sublist.append (nil_sublist _) ih
  | cons₂ a h ih =>
    simp only [List.sym2, map_cons, cons_append]
    exact cons₂ _ (append (Sublist.map _ h) ih)

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