English
For any indexing, the uncurry preimage distributes over sigma and pi-type: the preimage of the Pi-type equals a Pi-type of preimages.
Русский
Для любой индексации развёрнутое задание предобраза распределяется над сигмой и типом Pi: предобраз Pi-образ равен Pi-образу предобразов.
LaTeX
$$$\\Sigma.uncurry^{-1}'( (s \\sigma t).\\pi u ) = s.\\pi (i \\mapsto (t(i)).\\pi (j \\mapsto u\\langle i, j\\rangle))$$$
Lean4
theorem uncurry_preimage_sigma_pi {β : (i : ι) → α i → Type*} (s : Set ι) (t : (i : ι) → Set (α i))
(u : (p : (i : ι) × α i) → Set (β p.1 p.2)) :
Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi (fun i ↦ (t i).pi fun j ↦ u ⟨i, j⟩) :=
by
ext x
simp only [mem_preimage, mem_pi, mem_sigma_iff, and_imp]
exact ⟨fun h i hi j hj ↦ h ⟨i, j⟩ hi hj, fun h p hp1 hp2 ↦ h p.1 hp1 p.2 hp2⟩
