instHasUncurryPath — Mathlib

English

Any function φ : ∏ a, Path (x a) (y a) can be seen as a function α × I → X.

Русский

Любую функцию φ : ∀ a, Path (x a) (y a) можно рассматривать как функцию α × I → X.

LaTeX

$$$ \\text{HasUncurry} \\; (\\forall a:α,\; Path(x a)(y a)) \\; \\text{gives} \\; (a,t) \\mapsto (\\phi(a))(t). $$$

Lean4

/-- Any function `φ : Π (a : α), Path (x a) (y a)` can be seen as a function `α × I → X`. -/
instance instHasUncurryPath {α : Type*} {x y : α → X} : HasUncurry (∀ a : α, Path (x a) (y a)) (α × I) X :=
  ⟨fun φ p => φ p.1 p.2⟩

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