Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 16:35 a2e48025

View on Github →

feat(model_theory/fraisse): Defines Fraïssé classes (#12817) Defines the age of a structure (Mostly) characterizes the ages of countable structures Defines Fraïssé classes

Estimated changes

Modified src/model_theory/basic.lean

Modified src/model_theory/finitely_generated.lean

added theorem first_order.language.Structure.fg.cg

added theorem first_order.language.substructure.cg.sup

deleted theorem first_order.language.substructure.cg_sup

added theorem first_order.language.substructure.fg.sup

deleted theorem first_order.language.substructure.fg_sup

Created src/model_theory/fraisse.lean

added theorem first_order.language.age.countable_quotient

added theorem first_order.language.age.hereditary

added theorem first_order.language.age.is_equiv_invariant

added theorem first_order.language.age.joint_embedding

added def first_order.language.age

added def first_order.language.amalgamation

added def first_order.language.hereditary

added def first_order.language.joint_embedding