Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-06 06:03 faf16900

View on Github →

feat(model_theory/*): Any theory with infinite models has arbitrarily large models (#13980) Defines the theory distinct_constants_theory, indicating that a set of constants are distinct. Uses that theory to show that any theory with an infinite model has models of arbitrarily large cardinality.

Estimated changes

Modified src/model_theory/bundled.lean

added theorem first_order.language.Theory.Model.carrier_eq_coe

modified def first_order.language.Theory.Model.reduct

Modified src/model_theory/language_map.lean

Modified src/model_theory/satisfiability.lean

added theorem first_order.language.Theory.exists_large_model_of_infinite_model

added theorem first_order.language.Theory.is_satisfiable_union_distinct_constants_theory_of_card_le

added theorem first_order.language.Theory.is_satisfiable_union_distinct_constants_theory_of_infinite

Modified src/model_theory/semantics.lean

modified theorem first_order.language.Theory.model.mono

added theorem first_order.language.Theory.model.union

modified theorem first_order.language.Theory.model_iff_subset_complete_theory

modified theorem first_order.language.Theory.model_singleton_iff

added theorem first_order.language.Theory.model_union_iff

added theorem first_order.language.card_le_of_model_distinct_constants_theory

added theorem first_order.language.model_distinct_constants_theory

Modified src/model_theory/syntax.lean

added theorem first_order.language.directed_distinct_constants_theory

added def first_order.language.distinct_constants_theory

added theorem first_order.language.distinct_constants_theory_eq_Union

added theorem first_order.language.monotone_distinct_constants_theory