amalgamate — Mathlib

English

Get the amalgamation of a compatible family using a sheaf: amid a given IsSheafFor P R, x : FamilyOfElements P R, hx : x.Compatible, define amalgamate t = the chosen amalgamation from the existential witness.

Русский

Получить амальгамму совместимого семейства с использованием sheaf: имея t : IsSheafFor P R, x : FamilyOfElements P R, hx : x.Compatible, определить amalgamate как выбранную амальгамму из существующего свидетельства.

LaTeX

$$amalgamate (t : IsSheafFor P R) (x : FamilyOfElements P R) (hx : x.Compatible) : P.obj (op X)$$

Lean4

/-- Get the amalgamation of the given compatible family, provided we have a sheaf. -/
noncomputable def amalgamate (t : IsSheafFor P R) (x : FamilyOfElements P R) (hx : x.Compatible) : P.obj (op X) :=
  (t x hx).exists.choose

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