English
Every element of the direct limit arises from some component; i.e., for any z in the direct limit there exist i and x with z = of(i, x).
Русский
Каждый элемент прямого предела существует как образ некоторого элемента из компоненты: ∃ i, x такие что z = of(i, x).
LaTeX
$$$\\forall z \\in \\mathrm{DirectLimit} \\ G \\ f, \\; \\exists i\\exists x, \\; \\text{of}(R, \\iota, G, f, i, x) = z$$$
Lean4
/-- The relation on the direct sum that generates the additive congruence that defines the
colimit as a quotient. -/
inductive Eqv : DirectSum ι G → DirectSum ι G → Prop
| of_map {i j} (h : i ≤ j) (x : G i) : Eqv (DirectSum.lof R ι G i x) (DirectSum.lof R ι G j <| f i j h x)
