Theorems · Definition · logic and foundations

FirstOrder.Language.DirectedSystem.natLERec

{L : FirstOrder.Language} →
  {G' : ℕ → Type w} →
    [inst : (i : ℕ) → L.Structure (G' i)] →
      ((n : ℕ) → L.Embedding (G' n) (G' (n + 1))) → (m n : ℕ) → m ≤ n → L.Embedding (G' m) (G' n)

Given a chain of embeddings of structures indexed by ℕ, defines a DirectedSystem by composing them.

Defined in

Mathlib.ModelTheory.DirectLimit

Cited by

3 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.Structure