FirstOrder.Language.exists_elementarySubstructure_card_eq

theorem FirstOrder.Language.exists_elementarySubstructure_card_eq : ∀ (L : FirstOrder.Language) {M : Type w} [inst : Nonempty M] [inst : L.Structure M] (s : Set M) (κ : Cardinal.{w'}), Cardinal.aleph0 ≤ κ → Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} κ → Cardinal.lift.{w', max u v} L.card ≤ Cardinal.lift.{max u v, w'} κ → Cardinal.lift.{w, w'} κ ≤ Cardinal.lift.{w', w} (Cardinal.mk M) → ∃ S, s ⊆ ↑S ∧ Cardinal.lift.{w', w} (Cardinal.mk ↥S) = Cardinal.lift.{w, w'} κ

The **Downward Löwenheim–Skolem theorem** states that for any language `L`, if `M` is a type that has an `L`-structure (i.e., `M` is able to interpret the symbols of `L`), and `s` is a set within `M`, then given an infinite cardinal number `κ` such that the maximum of the cardinality of `s` and the cardinality of `L` is less than or equal to `κ`, and `κ` is less than or equal to the cardinality of `M`, there exists an elementary substructure `S` of `M` such that `s` is a subset of `S` and the cardinality of `S` is equal to `κ`. Here, cardinality is calculated by lifting it to the appropriate universe level. An elementary substructure is a subset that respects the same relations and operations as the larger structure. The theorem ensures that, given certain conditions on cardinality, we can always find such a "smaller copy" of our original structure.

More concisely: For any language `L`, given an `L`-structure `M` and a subset `s` of `M` with cardinality less than or equal to the infinite cardinal number `κ` that is less than or equal to the cardinality of `M`, there exists an elementary substructure `S` of `M` with cardinality `κ` containing `s`.