Commit 2022-05-05 22:29 c62dfe61

View on Github →

feat(model_theory/skolem): Downward Löwenheim–Skolem (#13723) Proves the Downward Löwenheim–Skolem theorem: If s is a set in an L-structure M and κ an infinite cardinal such that max (# s, L.card) ≤ κ and κ ≤ # M, then M has an elementary substructure containing s of cardinality κ.

Estimated changes

Modified src/model_theory/basic.lean

added theorem first_order.language.card_functions_sum

added theorem first_order.language.card_relations_sum

added theorem first_order.language.card_sum

Modified src/model_theory/skolem.lean

added theorem first_order.language.card_functions_sum_skolem₁

added theorem first_order.language.card_functions_sum_skolem₁_le

added theorem first_order.language.exists_elementary_substructure_card_eq

modified def first_order.language.skolem₁

modified theorem first_order.language.substructure.coe_sort_elementary_skolem₁_reduct

modified theorem first_order.language.substructure.skolem₁_reduct_is_elementary

Modified src/model_theory/syntax.lean