Commit 2023-05-13 14:37 9443ba42

View on Github →

feat: port ModelTheory.Bundled (#3933)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Bundled.lean

added def Equiv.bundledInduced

added def Equiv.bundledInducedEquiv

added def FirstOrder.Language.ElementarilyEquivalent.toModel

added def FirstOrder.Language.ElementarySubstructure.toModel

added def FirstOrder.Language.Theory.Model.bundled

added theorem FirstOrder.Language.Theory.ModelType.coe_of

added def FirstOrder.Language.Theory.ModelType.equivInduced

added def FirstOrder.Language.Theory.ModelType.of

added def FirstOrder.Language.Theory.ModelType.reduct

added def FirstOrder.Language.Theory.ModelType.subtheoryModel

added def FirstOrder.Language.Theory.ModelType.ulift

added structure FirstOrder.Language.Theory.ModelType

added theorem FirstOrder.Language.Theory.coe_of