Commit 2022-04-13 10:56 647aa5be

View on Github →

feat(model_theory/fraisse): Defines ultrahomogeneous structures, fixes Fraïssé limit definition (#12994) Defines ultrahomogeneous structures Fixes the definition of a Fraïssé limit to require ultrahomogeneity Completes the characterization of when a class is the age of a countable structure.

Estimated changes

Modified src/model_theory/fraisse.lean

added theorem first_order.language.age.nonempty

deleted theorem first_order.language.age_fraisse_limit

added theorem first_order.language.exists_countable_is_age_of_iff

added theorem first_order.language.is_fraisse_limit.is_fraisse

added structure first_order.language.is_fraisse_limit

added theorem first_order.language.is_ultrahomogeneous.age_is_fraisse

added theorem first_order.language.is_ultrahomogeneous.amalgamation_age

added def first_order.language.is_ultrahomogeneous