instFiniteObjCompFintypeCatIncl — Mathlib

English

For a functor K : J ⥤ FintypeCat with J small, each object (K ⋙ incl) obj j is finite.

Русский

Для функторa K : J ⥤ FintypeCat и малой J каждый объект (K ⋙ incl) obj j конечен.

LaTeX

$$$\\forall j,\\ Finite\\big((K\\;\\text{comp}\\; \\mathrm{incl}).\\mathrm{obj}\\; j\\big)$$$

Lean4

instance {J : Type} [SmallCategory J] (K : J ⥤ FintypeCat.{u}) (j : J) : Finite ((K ⋙ FintypeCat.incl.{u}).obj j) :=
  by
  simp only [comp_obj, FintypeCat.incl_obj]
  infer_instance

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