mathlib

faf16900 - feat(model_theory/*): Any theory with infinite models has arbitrarily large models (#13980)

feat(model_theory/*): Any theory with infinite models has arbitrarily large models (#13980) Defines the theory `distinct_constants_theory`, indicating that a set of constants are distinct. Uses that theory to show that any theory with an infinite model has models of arbitrarily large cardinality.