revzip_powersetAux_perm_aux' — Mathlib

English

There is a permutation between revzip(powersetAux l) and revzip(powersetAux' l).

Русский

Существует перестановка между revzip(powersetAux l) и revzip(powersetAux' l).

LaTeX

$$$ \\mathrm{revzip}(\\mathrm{powersetAux}(l)) \\sim \\mathrm{revzip}(\\mathrm{powersetAux}'(l)) $$$

Lean4

theorem revzip_powersetAux_perm_aux' {l : List α} : revzip (powersetAux l) ~ revzip (powersetAux' l) :=
  by
  haveI := Classical.decEq α
  rw [revzip_powersetAux_lemma l revzip_powersetAux, revzip_powersetAux_lemma l revzip_powersetAux']
  exact powersetAux_perm_powersetAux'.map _

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