Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-23 10:41 2308b53c

View on Github →

feat(model_theory/terms_and_formulas): Make Theory.model a class (#12867) Makes Theory.model a class

Estimated changes

Modified src/model_theory/elementary_maps.lean

Modified src/model_theory/terms_and_formulas.lean

deleted theorem first_order.language.Theory.is_satisfiable.some_model_models

modified theorem first_order.language.Theory.model.mono

deleted def first_order.language.Theory.model

modified def first_order.language.Theory.models_bounded_formula

modified theorem first_order.language.Theory.models_formula_iff

modified theorem first_order.language.Theory.models_sentence_iff

added theorem first_order.language.Theory.realize_sentence_of_mem

modified theorem first_order.language.Theory.semantically_equivalent.refl

modified theorem first_order.language.Theory.semantically_equivalent.symm

modified theorem first_order.language.Theory.semantically_equivalent.trans

Modified src/model_theory/ultraproducts.lean