mathlib3

4b9e57b1 - feat(model_theory/satisfiability): Upward Löwenheim–Skolem (#13982)

feat(model_theory/satisfiability): Upward Löwenheim–Skolem (#13982) `first_order.language.Theory.exists_elementary_embedding_card_eq` proves the Upward Löwenheim–Skolem Theorem: every infinite `L`-structure `M` elementarily embeds into an `L`-structure of a given cardinality if that cardinality is larger than the cardinalities of `L` and `M`.