revzip_powersetAux — Mathlib

English

If x is in revzip(powersetAux(l)), then the sum of its components equals the multiset corresponding to l.

Русский

Если x ∈ revzip(powersetAux(l)), тогда x.fst + x.snd = ↑l.

LaTeX

$$$ \\forall l, \\forall x \\in \\mathrm{revzip}(\\mathrm{powersetAux}(l)),\; x_1 + x_2 = \\uparrow l $$$

Lean4

theorem revzip_powersetAux {l : List α} ⦃x⦄ (h : x ∈ revzip (powersetAux l)) : x.1 + x.2 = ↑l :=
  by
  rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h
  simp only [Prod.map_apply, Prod.exists] at h
  rcases h with ⟨l₁, l₂, h, rfl, rfl⟩
  exact Quot.sound (revzip_sublists _ _ _ h)

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