revzip_powersetAux' — Mathlib

English

For any l, if x is in revzip(powersetAux'(l)) then x.1 + x.2 = ↑l.

Русский

Для любого l, если x ∈ revzip(powersetAux'(l)), то x.1 + x.2 = ↑l.

LaTeX

$$$ \\forall l, \\forall x \\in \\mathrm{revzip}(\\mathrm{powersetAux}'(l)),\n\\; 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', ← 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)

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