hasUncurryInduction — Mathlib

English

If HasUncurry β γ δ holds, then HasUncurry (α → β) (α × γ) δ holds with uncurry defined by uncurry f (a, c) = (f a) c.

Русский

Если имеется раскрытие для β, γ, δ, то существует раскрытие для α → β с областью α × γ → δ, заданное как uncurry f (a, c) = (f a) c.

LaTeX

$$$ \\forall {α β γ δ} [HasUncurry β γ δ],\\n HasUncurry (α \\to β) (α \\times γ) δ $ and the uncurry is given by $ (uncurry f)(a,c) = (f a) c $$$

Lean4

instance hasUncurryInduction [HasUncurry β γ δ] : HasUncurry (α → β) (α × γ) δ :=
  ⟨fun f p ↦ ↿(f p.1) p.2⟩

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