eventualRange — Mathlib

English

For a functor F : J ⥤ Type, the eventual range at j is the intersection of all ranges of F.map f for all i ⟶ j.

Русский

Для данного функторa F : J ⥤ Type, предельный диапазон в точке j есть как пересечение всех образов F.map f для всех i ⟶ j.

LaTeX

$$$ \mathrm{eventualRange}(j) = \bigcap_{i,f:i\to j} \mathrm{range}(F.map f) $$$

Lean4

/-- The eventual range of the functor `F : J ⥤ Type v` at index `j : J` is the intersection
of the ranges of all maps `F.map f` with `i : J` and `f : i ⟶ j`. -/
def eventualRange (j : J) :=
  ⋂ (i) (f : i ⟶ j), range (F.map f)

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