Theorems · Definition · logic and foundations

FirstOrder.Language.IsFraisseLimit.recOn

{L : FirstOrder.Language} →
  {K : Set (CategoryTheory.Bundled L.Structure)} →
    {M : Type w} →
      [inst : L.Structure M] →
        [inst_1 : Countable ((l : ℕ) × L.Functions l)] →
          [inst_2 : Countable M] →
            {motive : FirstOrder.Language.IsFraisseLimit K M → Sort u_1} →
              (t : FirstOrder.Language.IsFraisseLimit K M) →
                ((ultrahomogeneous : L.IsUltrahomogeneous M) → (age : L.age M = K) → motive ⋯) → motive t

Defined in

Mathlib.ModelTheory.Fraisse

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureCountableCountable