kerase — Mathlib

English

If l1 and l2 are lists with NodupKeys and l1 isPerm l2, then kerase a l1 isPerm kerase a l2. In other words, kerase respects permutation when NodupKeys hold.

Русский

Если списки l1 и l2 эквивалентны по перестановкам и у них есть безповторные ключи, то kerase a l1 эквивал kerase a l2.

LaTeX

$$∀ {a} {l₁ l₂}, l₁.NodupKeys → l₁ ~ l₂ → kerase a l₁ ~ kerase a l₂$$

Lean4

theorem kerase {a : α} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys) : l₁ ~ l₂ → kerase a l₁ ~ kerase a l₂ :=
  by
  apply Perm.eraseP
  apply (nodupKeys_iff_pairwise.1 nd).imp
  intros; simp_all

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