Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-31 16:09 f1ae6206

View on Github →

feat(model_theory/bundled, satisfiability): Bundled models (#12945) Defines Theory.Model, a type of nonempty bundled models of a particular theory. Refactors satisfiability in terms of bundled models.

Estimated changes

Modified src/model_theory/basic.lean

added def first_order.language.trivial_unit_structure

Modified src/model_theory/bundled.lean

added theorem first_order.language.Theory.Model.coe_of

added def first_order.language.Theory.Model.of

added structure first_order.language.Theory.Model

added theorem first_order.language.Theory.coe_of

added def first_order.language.Theory.model.bundled

Modified src/model_theory/satisfiability.lean

deleted def first_order.language.Theory.is_satisfiable.some_model

modified def first_order.language.Theory.is_satisfiable

deleted theorem first_order.language.Theory.semantically_equivalent.some_model_realize_bd_iff

deleted theorem first_order.language.Theory.semantically_equivalent.some_model_realize_iff

Modified src/model_theory/semantics.lean

Modified src/model_theory/ultraproducts.lean