English
Let {G i} be a directed system with direct limit. For every rational q and index i, the image of q in the direct limit coincides with the class of the pair (i, q). In particular, the embedding of ℚ into the direct limit is independent of the chosen index.
Русский
Пусть дано направленное семейство модулей {G_i} с пределом по направлению. Для каждого рационального числа q и индекса i образ q в прямом пределe совпадает с клишею пары (i, q). Равенство означает независимость вложения ℚ в предел от выбора индекса.
LaTeX
$$$\\forall q \\in \\mathbb{Q}, \\; \\forall i, \\ (q : \\mathrm{DirectLimit} \\ G \\ f) = \\llbracket \\langle i, q \\rangle \\rrbracket,$$$
Lean4
theorem ratCast_def (q : ℚ) (i) : (q : DirectLimit G f) = ⟦⟨i, q⟩⟧ :=
map₀_def _ _ (fun _ _ _ ↦ map_ratCast _ _) _
