uncurry_preimage_prod_pi — Mathlib

English

Uncurrying a preimage of a product over s×t decomposes into a product of preimages over s and t.

Русский

Развёртывание предобраза произведения над s×t разлагается на произведение предобразов над s и над t.

LaTeX

$$$$ \\mathrm{uncurry}^{-1}'( (s \\times^\\! t).\\pi u ) = s.\\pi(\\lambda i. t.\\pi(\\lambda j. u\\langle i,j\\rangle)). $$$$

Lean4

theorem uncurry_preimage_prod_pi {κ α : Type*} (s : Set ι) (t : Set κ) (u : ι × κ → Set α) :
    Function.uncurry ⁻¹' (s ×ˢ t).pi u = s.pi (fun i ↦ t.pi fun j ↦ u ⟨i, j⟩) := by grind

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