mem_eventualRange_iff — Mathlib

English

Let F : J ⥤ Type v be a functor from a small category J to types. For any object j, an element x ∈ F.obj j lies in the eventual range F.eventualRange(j) exactly when, for every i and every morphism f : i ⟶ j, x is in the image of F.map f.

Русский

Пусть F : J ⥤ Type v — функтор из малой категории J в типы. Пусть для каждого объекта j элемент x ∈ F.obj j принадлежит к предельному диапазону F.eventualRange(j) тогда и только тогда, для каждого i и каждого морфизма f : i ⟶ j, элемент x принадлежит образу F.map f.

LaTeX

$$$\forall j, \forall x \in F.obj j,\ x \in F.eventualRange(j) \iff \forall i \forall f : i \to j, x \in \mathrm{range}(F.map f).$$$

Lean4

theorem mem_eventualRange_iff {x : F.obj j} : x ∈ F.eventualRange j ↔ ∀ ⦃i⦄ (f : i ⟶ j), x ∈ range (F.map f) :=
  mem_iInter₂

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