Commit 2024-08-16 05:48 9045ac05

View on Github →

feat(ModelTheory): Fraïssé limits are unique (#9967) Prove that Fraïsse limits are unique up to equivalence.

Estimated changes

Modified Mathlib/ModelTheory/DirectLimit.lean

Modified Mathlib/ModelTheory/Fraisse.lean

added theorem FirstOrder.Language.IsFraisseLimit.nonempty_equiv

added theorem FirstOrder.Language.IsUltrahomogeneous.extend_embedding

added theorem FirstOrder.Language.age.fg_substructure

added theorem FirstOrder.Language.age.has_representative_as_substructure

added theorem FirstOrder.Language.isUltrahomogeneous_iff_IsExtensionPair

Modified Mathlib/ModelTheory/Substructures.lean

added theorem FirstOrder.Language.Substructure.closure_iUnion

deleted theorem FirstOrder.Language.Substructure.closure_unionᵢ

added theorem FirstOrder.Language.Substructure.iSup_eq_closure

added theorem FirstOrder.Language.Substructure.mem_iSup_of_directed

added theorem FirstOrder.Language.Substructure.mem_sSup_of_directedOn