uncurry_bicompr — Mathlib

English

If f : γ → δ → ε, g : α → γ, h : β → δ, then 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_bicompr (f : α → β → γ) (g : γ → δ) : uncurry (g ∘₂ f) = g ∘ uncurry f :=
  rfl

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