uncurry_mulSingle_mulSingle — Mathlib

English

Uncurrying the nested single injection recovers the canonical single injection corresponding to the pair (a,b).

Русский

Раскругив последовательную единичную инъекцию восстанавливает каноническую инъекцию, соответствующую паре (a,b).

LaTeX

$$$\Sigma.uncurry(\Pi.mulSingle a (\Pi.mulSingle b x)) = \Pi.mulSingle (\Sigma.mk a b) x$$$

Lean4

@[to_additive (attr := simp)]
theorem uncurry_mulSingle_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)] (a : α) (b : β a)
    (x : γ a b) : Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle (Sigma.mk a b) x := by
  rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]

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