isGroupoidPi — Mathlib

English

The dependent product of a family of groupoids is again a groupoid.

Русский

Зависимое произведение семейства групоидов снова образует групоид.

LaTeX

$$$\mathrm{IsGroupoid}\big(\prod_{i\in I} J(i)\big)$$$

Lean4

instance isGroupoidPi {I : Type u} {J : I → Type u₂} [∀ i, Category.{v} (J i)] [∀ i, IsGroupoid (J i)] :
    IsGroupoid (∀ i : I, J i) where all_isIso f := (isIso_pi_iff f).mpr (fun _ ↦ inferInstance)

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