mathlib3

50ff59ad - feat(model_theory/skolem, satisfiability): A weak Downward Loewenheim Skolem (#13141)

feat(model_theory/skolem, satisfiability): A weak Downward Loewenheim Skolem (#13141) Defines a language and structure with built-in Skolem functions for a particular language Proves a weak form of Downward Loewenheim Skolem: every structure has a small (in the universe sense) elementary substructure Shows that `T` having a model in any universe implies `T.is_satisfiable`.