localGeneratorsDataOfIsFiniteType

English

If M is finite-type, then for each i, the generators at X_i form a finite set.

Русский

Если M имеет конечный тип, тогда порождающие на X_i образуют конечное множество.

LaTeX

$$$\forall i, \text{Finite}(M.localGeneratorsDataOfIsFiniteType.generators i).I$$$

Lean4

/-- A choice of local generators when `M` is a sheaf of modules of finite type. -/
noncomputable def localGeneratorsDataOfIsFiniteType : M.LocalGeneratorsData :=
  h.exists_localGeneratorsData.choose

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