English
If every bonding map f_i_j is injective, then for each index i the canonical map from F_i to the direct limit D is injective.
Русский
Если все связующие отображения f_i_j инъективны, то для каждого индекса i каноническое отображение F_i в прямой предел D инъективно.
LaTeX
$$$\\forall i,\\; \\mathrm{Injective}\\big(\\lambda x. \\big\\llbracket\\langle i,x\\rangle\\big\\rrbracket\\big) \\quad\\text{where } \\big\\llbracket\\langle i,x\\rangle\\big\\rrbracket\\in \\mathrm{DirectLimit}(F,f)$$$
Lean4
theorem mk_injective (h : ∀ i j hij, Function.Injective (f i j hij)) (i) :
Function.Injective fun x ↦ (⟦⟨i, x⟩⟧ : DirectLimit F f) := fun _ _ eq ↦
have ⟨_, _, _, eq⟩ := Quotient.eq.mp eq;
h _ _ _ eq
