kunion — Mathlib

English

If l1 ~ l2 and l3 ~ l4, and l3 has nodupkeys, then combining the left components via kunion preserves permutation.

Русский

Если l1 ~ l2 и l3 ~ l4, и у l3 есть NodupKeys, то левый kunion сохраняет перестановку.

LaTeX

$$$\\forall l_1,l_2,l_3,l_4:\\text{List}(\\Sigma \\beta),\\; l_3.\\NodupKeys \\to (l_1 \\sim l_2) \\to (l_3 \\sim l_4) \\to (kunion l_1 l_3) \\sim (kunion l_2 l_4)$$$

Lean4

theorem kunion {l₁ l₂ l₃ l₄ : List (Sigma β)} (nd₃ : l₃.NodupKeys) (p₁₂ : l₁ ~ l₂) (p₃₄ : l₃ ~ l₄) :
    kunion l₁ l₃ ~ kunion l₂ l₄ :=
  (p₁₂.kunion_right l₃).trans (p₃₄.kunion_left l₂ nd₃)

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