Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 10:12 892e6113

View on Github →

feat(model_theory/*): Facts about countability of first-order structures (#12819) Shows that in a countable language, a structure is countably generated if and only if it is countable.

Estimated changes

Modified src/data/equiv/encodable/basic.lean

Modified src/model_theory/basic.lean

added def first_order.language.card

added theorem first_order.language.card_eq_card_functions_add_card_relations

added theorem first_order.language.card_functions_le_omega

added theorem first_order.language.card_le_omega

added theorem first_order.language.encodable.countable

added theorem first_order.language.encodable.countable_functions

Modified src/model_theory/finitely_generated.lean

added theorem first_order.language.Structure.cg_iff_countable

modified theorem first_order.language.substructure.cg_closure

added theorem first_order.language.substructure.cg_iff_countable

Modified src/model_theory/substructures.lean

added theorem set.countable.substructure_closure

Modified src/model_theory/terms_and_formulas.lean

added theorem first_order.language.term.card_le_omega