Theorems · Theorem · logic and foundations

FirstOrder.Language.exists_countable_is_age_of_iff

∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [Countable ((l : ℕ) × L.Functions l)],
  (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (L.Equiv ↑M ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧
          (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) ∧
            FirstOrder.Language.Hereditary K ∧ FirstOrder.Language.JointEmbedding K

Defined in

Mathlib.ModelTheory.Fraisse

Cited by

0 results in Mathlib

Foundations

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

Assumes

Countable