English
Every element of the direct limit arises from some component; i.e., z ∈ DirectLimit G f implies ∃ i ∃ x, of G f i x = z.
Русский
Каждый элемент прямого предела проистекает из некоторой компоненты; то есть каждый элемент предела равен of i x для некоторого i и x.
LaTeX
$$$\exists i\,\exists x:\; \text{of}(G,f,i,x) = z$$$
Lean4
theorem map_comp (g₁ : (i : ι) → G i →+ G' i) (g₂ : (i : ι) → G' i →+ G'' i)
(hg₁ : ∀ i j h, (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
(hg₂ : ∀ i j h, (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)) :
((map g₂ hg₂).comp (map g₁ hg₁) : DirectLimit G f →+ DirectLimit G'' f'') =
(map (fun i ↦ (g₂ i).comp (g₁ i)) fun i j h ↦ by
rw [AddMonoidHom.comp_assoc, hg₁ i, ← AddMonoidHom.comp_assoc, hg₂ i, AddMonoidHom.comp_assoc] :
DirectLimit G f →+ DirectLimit G'' f'') :=
by ext; simp
