abs — Mathlib

English

The abstraction function abs for Pi maps a Pi.P F α-object to a Pi F α-object by evaluating the function at the appropriate coordinate and using the family of QPF-abs on fibers.

Русский

Абстракция для Pi переводит Pi.P F α-объект в Pi F α-объект, вычисляя компоненту на соответствующей координате и применяя семейство QPF-abs к волокнам.

LaTeX

$$$\\\\mathrm{abs} : (\\\\Pi.P F).Obj α \\\\to (\\\\Pi F).Obj α, \\\\mathrm{abs}⟨a, f⟩ = \\\\lambda x. \\\\mathrm{abs} ⟨a x, \\\\lambda i y. f i ⟨x, y⟩⟩.$$$

Lean4

/-- abstraction function for dependent products -/
protected def abs ⦃α⦄ : Pi.P F α → Pi F α
  | ⟨a, f⟩ => fun x => MvQPF.abs ⟨a x, fun i y => f i ⟨_, y⟩⟩

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