mathlib3

003701f0 - feat(model_theory/substructures): Facts about substructures (#12258)

feat(model_theory/substructures): Facts about substructures (#12258) Shows that `closure L s` can be viewed as the set of realizations of terms over `s`. Bounds the cardinality of `closure L s` by the cardinality of the type of terms. Characterizes `closure L[[A]] s`. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>