Theorems · Theorem · logic and foundations

FirstOrder.Language.DirectedSystem.coe_natLERec

∀ {L : FirstOrder.Language} {G' : ℕ → Type w} [inst : (i : ℕ) → L.Structure (G' i)]
  (f' : (n : ℕ) → L.Embedding (G' n) (G' (n + 1))) (m n : ℕ) (h : m ≤ n),
  ⇑(FirstOrder.Language.DirectedSystem.natLERec f' m n h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a

Defined in

Mathlib.ModelTheory.DirectLimit

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.Structure