Theorems · Theorem · logic and foundations

FirstOrder.Language.exists_cg_is_age_of

∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)},
  K.Nonempty →
    (Quotient.mk' '' K).Countable →
      (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) →
        FirstOrder.Language.Hereditary K →
          FirstOrder.Language.JointEmbedding K → ∃ M, FirstOrder.Language.Structure.CG L ↑M ∧ L.age ↑M = K

Sufficient conditions for a class to be the age of a countably-generated structure.

Defined in: Mathlib.ModelTheory.Fraisse
Cited by: 1 results in Mathlib
Foundations: Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites37

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.Elemproof · cited by 7,166
Set.imagestatement and proof · cited by 5,609
Set.rangeproof · cited by 4,705
Set.Nonemptystatement and proof · cited by 2,627
FirstOrder.Languagestatement and proof · cited by 1,084
FirstOrder.Language.Structurestatement and proof · cited by 775
CategoryTheory.Bundled.αstatement and proof · cited by 736
Set.Countablestatement and proof · cited by 545
Nonempty.someproof · cited by 340
subset_antisymmproof · cited by 150
Quotient.outproof · cited by 141

Cited by1

Results whose statement or proof uses this declaration.

FirstOrder.Language.exists_countable_is_age_of_iffproof · cited by 0