directedSystem — Mathlib

English

The family of embeddings φm,n defined by natLERec equips the family (G′i) with a directed-system structure over i ∈ ℕ; composing along indices respects directed-system axioms.

Русский

Семейство вложений φm,n, заданное natLERec, образует направленную систему для семейства G′i; композиция вдоль индексов удовлетворяет аксиомам направленной системы.

LaTeX

$$$\\text{The family }\\{\\varphi_{m,n}\\}_{m\\le n}\\text{ with }\\varphi_{m,n+1}=f'_n\\circ\\varphi_{m,n}\\text{ defines a directed system: }\\varphi_{m,n}=\\varphi_{k,n}\\circ\\varphi_{m,k}\\ (m\\le k\\le n).$$$

Lean4

instance directedSystem : DirectedSystem G' fun i j h => natLERec f' i j h :=
  ⟨fun _ _ => congr (congr rfl (Nat.leRecOn_self _)) rfl, fun _ _ _ hij hjk => by simp [Nat.leRecOn_trans hij hjk]⟩

Похожие утверждения