curry_mulSingle — Mathlib

English

The curry of the Pi.mulSingle corresponds to nested single injections in Sigma-curry form.

Русский

Карри-образ Π.mulSingle соответствует вложенным единичным инъекциям в форме карри Sigma.

LaTeX

$$$\Sigma\text{-}curry(\Pi.mulSingle i x) = \Pi.mulSingle i.1 (\Pi.mulSingle i.2 x)$$$

Lean4

@[to_additive (attr := simp)]
theorem curry_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)] (i : Σ a, β a) (x : γ i.1 i.2) :
    Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.1 (Pi.mulSingle i.2 x) := by
  simp only [Pi.mulSingle, Sigma.curry_update, Sigma.curry_one, Pi.one_apply]

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