Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-14 16:17 0602c598

View on Github →

refactor(model_theory/*): Use countable in model theory (#16496) Uses countable instead of custom classes in the model theory library.

Estimated changes

Modified src/model_theory/basic.lean

deleted theorem first_order.language.card_functions_le_aleph_0

deleted theorem first_order.language.card_le_aleph_0

deleted theorem first_order.language.encodable.countable

deleted theorem first_order.language.encodable.countable_functions

Modified src/model_theory/encoding.lean

deleted theorem first_order.language.term.card_le_aleph_0

Modified src/model_theory/finitely_generated.lean

modified theorem first_order.language.Structure.cg_iff_countable

modified theorem first_order.language.substructure.cg_iff_countable

Modified src/model_theory/fraisse.lean

modified theorem first_order.language.age.countable_quotient

modified theorem first_order.language.exists_countable_is_age_of_iff

modified theorem first_order.language.is_fraisse_limit.is_fraisse

modified structure first_order.language.is_fraisse_limit

modified theorem first_order.language.is_ultrahomogeneous.age_is_fraisse

Modified src/model_theory/substructures.lean

modified theorem set.countable.substructure_closure