Commit 2023-07-07 17:05 b07960ca

View on Github →

feat: port ModelTheory.Fraisse (#4565)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/ModelTheory/DirectLimit.lean

deleted theorem FirstOrder.Language.DirectLimit.cG

added theorem FirstOrder.Language.DirectLimit.cg

Created Mathlib/ModelTheory/Fraisse.lean

added def FirstOrder.Language.Amalgamation

added theorem FirstOrder.Language.Embedding.age_subset_age

added theorem FirstOrder.Language.Equiv.age_eq_age

added theorem FirstOrder.Language.Hereditary.is_equiv_invariant_of_fG

added def FirstOrder.Language.Hereditary

added theorem FirstOrder.Language.IsFraisseLimit.isFraisse

added structure FirstOrder.Language.IsFraisseLimit

added theorem FirstOrder.Language.IsUltrahomogeneous.age_isFraisse

added theorem FirstOrder.Language.IsUltrahomogeneous.amalgamation_age

added def FirstOrder.Language.IsUltrahomogeneous

added def FirstOrder.Language.JointEmbedding

added theorem FirstOrder.Language.Structure.FG.mem_age_of_equiv

added theorem FirstOrder.Language.age.countable_quotient

added theorem FirstOrder.Language.age.hereditary

added theorem FirstOrder.Language.age.is_equiv_invariant

added theorem FirstOrder.Language.age.jointEmbedding

added theorem FirstOrder.Language.age.nonempty

added def FirstOrder.Language.age

added theorem FirstOrder.Language.age_directLimit

added theorem FirstOrder.Language.exists_cg_is_age_of

added theorem FirstOrder.Language.exists_countable_is_age_of_iff