Theorems · Theorem · logic and foundations

FirstOrder.Language.age_directLimit

∀ {L : FirstOrder.Language} {ι : Type w} [inst : Preorder ι] [inst_1 : IsDirectedOrder ι] [inst_2 : Nonempty ι]
  (G : ι → Type (max w w')) [inst_3 : (i : ι) → L.Structure (G i)] (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j))
  [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)], L.age (FirstOrder.Language.DirectLimit G f) = ⋃ i, L.age (G i)

The age of a direct limit of structures is the union of the ages of the structures.

Defined in

Mathlib.ModelTheory.Fraisse

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderIsDirectedOrderNonemptyFirstOrder.Language.StructureDirectedSystem