instFiniteIOverXLocalGeneratorsDataOfIsFiniteTypeGenerators

English

For a finite-type M, the index I has a finite fiber: each generator’s index set is finite.

Русский

Для конечного типа M множество индексов, соответствующее данным порождения, конечно.

LaTeX

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

Lean4

instance (i : M.localGeneratorsDataOfIsFiniteType.I) : Finite (M.localGeneratorsDataOfIsFiniteType.generators i).I :=
  h.exists_localGeneratorsData.choose_spec i

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