mathlib3

ed688546 - feat(model_theory/*): Theory of nonempty structures and bundling elementary substructures (#13118)

feat(model_theory/*): Theory of nonempty structures and bundling elementary substructures (#13118) Defines a sentence and theory to indicate a structure is nonempty Defines a map to turn elementary substructures of a bundled model into bundled models