objAppend1 — Mathlib

English

Constructing an element of the extended object P.Obj (α ::: β) from an edge a, a tail map f′ and a tail f : P.last.B a → β, by composing into a splitFun.

Русский

Построение элемента расширенного объекта P.Obj (α ::: β) из элемента a, хвостовой карты f′ и хвоста f : P.last.B a → β через композицию в splitFun.

LaTeX

$$$\text{objAppend1}\ {\alpha}\ {\beta}\ (a)\ (f')\ (f) = ⟨a, splitFun\ (f')\ f⟩$$$

Lean4

/-- Constructor of a value of `P.obj (α ::: β)` from components.
Useful to avoid complicated type annotation -/
abbrev objAppend1 {α : TypeVec n} {β : Type u} (a : P.A) (f' : P.drop.B a ⟹ α) (f : P.last.B a → β) : P (α ::: β) :=
  ⟨a, splitFun f' f⟩

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