mathlib3

892e6113 - feat(model_theory/*): Facts about countability of first-order structures (#12819)

feat(model_theory/*): Facts about countability of first-order structures (#12819) Shows that in a countable language, a structure is countably generated if and only if it is countable.