familyOfElements — Mathlib

English

There is a canonical FamilyOfElements hx.familyOfElements associated to hx, which is the explicit realization of a compatible family of elements over the presieve of arrows.

Русский

Существует каноническое семейство элементов hx.familyOfElements, связанное с hx, являющееся явной реализацией совместимого семейства элементов над пресивом стрелок.

LaTeX

$$$\text{familyOfElements} : \mathrm{FamilyOfElements}(P, \mathrm{ofArrows}(X,\pi))$$$

Lean4

/-- A `FamilyOfElements` associated to an explicit family of elements.
-/
noncomputable def familyOfElements : FamilyOfElements P (ofArrows X π) :=
  (exists_familyOfElements hx).choose

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