uncurry_bicompl — Mathlib

English

For f : γ → δ → ε, g : α → γ, h : β → δ, uncurry (bicompl f g h) = uncurry f ∘ Prod.map g h.

Русский

Для f : γ → δ → ε, g : α → γ, h : β → δ: uncurry (bicompl f g h) = uncurry f ∘ Prod.map g h.

LaTeX

$$$ \\forall {f : \\gamma \\to \\delta \\to \\epsilon} {g : \\alpha \\to \\gamma} {h : \\beta \\to \\delta},\\n \\operatorname{uncurry}(\\operatorname{bicompl} f g h) = \\operatorname{uncurry} f \\circ \\operatorname{Prod.map} g h $$$

Lean4

theorem uncurry_bicompl (f : γ → δ → ε) (g : α → γ) (h : β → δ) : uncurry (bicompl f g h) = uncurry f ∘ Prod.map g h :=
  rfl

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