revzip_powersetAux_perm — Mathlib

English

For lists l1, l2 with l1 Perm l2, revzip(powersetAux l1) Perm revzip(powersetAux l2).

Русский

Если l1Perm l2, то revzip(powersetAux l1) Perm revzip(powersetAux l2).

LaTeX

$$$ \\forall l_1,l_2,\\; l_1 \\sim l_2 \\Rightarrow \\mathrm{revzip}(\\mathrm{powersetAux}(l_1)) \\sim \\mathrm{revzip}(\\mathrm{powersetAux}(l_2)) $$$

Lean4

theorem revzip_powersetAux_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) : revzip (powersetAux l₁) ~ revzip (powersetAux l₂) :=
  by
  haveI := Classical.decEq α
  simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]
  exact (powersetAux_perm p).map _

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