English
Let G′ be a family of structures indexed by the natural numbers, together with embeddings f′n: G′n → G′n+1 forming a chain. Then this chain determines a directed system on the family (G′n) via the embeddings φm,n, defined by composing the successive embeddings along the interval [m, n). In particular, for m ≤ n, φm,n is obtained by composing f′m, f′m+1, …, f′n−1, and these embeddings satisfy φm,m = id and φm,n+φn,p = φm,p.
Русский
Пусть G′ — это семейство структур, индексируемых по натуральным числам, вместе с вложениями f′n: G′n → G′n+1, образующими цепь. Тогда эта цепь порождает направленную систему для семейства (G′n): вложения φm,n получаются как композиция вложений вдоль промежутка [m, n). В частности, φm,m = id и φm,p = φn,p ∘ φm,n при m ≤ n ≤ p.
LaTeX
$$$\\forall m,n \\in \\mathbb{N},\\ m \\le n \\Rightarrow G'_m \\hookrightarrow_L G'_n \\\\[2mm] \\text{with } \\varphi_{m,m}=\\mathrm{id}_{G'_m},\\ \\varphi_{m,n+1}=f'_n\\circ \\varphi_{m,n},\\ \\text{and } \\varphi_{m,n}=\\varphi_{k,n}\\circ\\varphi_{m,k} \\text{ for } m\\le k\\le n.$$$
Lean4
/-- Given a chain of embeddings of structures indexed by `ℕ`, defines a `DirectedSystem` by
composing them. -/
def natLERec (m n : ℕ) (h : m ≤ n) : G' m ↪[L] G' n :=
Nat.leRecOn h (@fun k g => (f' k).comp g) (Embedding.refl L _)
