Commit 2022-05-27 17:02 4b9e57b1
View on Github →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.