Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 17:30 f53b2399

View on Github →

feat(model_theory/fraisse): Construct Fraïssé limits (#12138) Constructs Fraïssé limits (nonuniquely)

Estimated changes

Modified docs/references.bib

Modified src/model_theory/direct_limit.lean

added theorem first_order.language.direct_limit.cg

added theorem first_order.language.directed_system.coe_nat_le_rec

added def first_order.language.directed_system.nat_le_rec

Modified src/model_theory/finitely_generated.lean

Modified src/model_theory/fraisse.lean

added theorem first_order.language.Structure.fg.mem_age_of_equiv

added theorem first_order.language.age_direct_limit

added theorem first_order.language.age_fraisse_limit

added theorem first_order.language.embedding.age_subset_age

added theorem first_order.language.equiv.age_eq_age

added theorem first_order.language.exists_cg_is_age_of

added theorem first_order.language.hereditary.is_equiv_invariant_of_fg