English
Downward Löwenheim–Skolem: there exists an elementary substructure of size κ containing a given set.
Русский
Пусть s ⊆ M и κ — бесконечная кардинальность с κ ≥ max(|s|, card(L)) и κ ≤ |M|. Тогда существует элементарная подструктура S M, содержащая s, такая что |S| = κ.
LaTeX
$$$\exists S : L.\text{ElementalSubstructure } M,\; s \subseteq S \land lift_{w'}(|S|) = lift_{w}(κ)$$$
Lean4
theorem card_functions_sum_skolem₁ : #(Σ n, (L.sum L.skolem₁).Functions n) = #(Σ n, L.BoundedFormula Empty (n + 1)) :=
by
simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']
conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
rw [add_comm, add_eq_max, max_eq_left]
· refine sum_le_sum _ _ fun n => ?_
rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]
refine ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => ?_⟩⟩
rcases h with ⟨rfl, ⟨rfl⟩⟩
rfl
· rw [← mk_sigma]
exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy => (Sigma.mk.inj_iff.1 xy).1)
