English
If M is infinite and satisfies T, then the union of T with the distinct-constants theory is satisfiable.
Русский
Если M бесконечно, и удовлетворяет T, тогда объединение T с теорией различныx констант удовлетворимо.
LaTeX
$$$$ \\text{If } M \\text{ is infinite and models } T, \\; ((L.lhomWithConstants α).onTheory T \\cup L.distinctConstantsTheory s).IsSatisfiable $$$$
Lean4
theorem isSatisfiable_union_distinctConstantsTheory_of_infinite (T : L.Theory) (s : Set α) (M : Type w') [L.Structure M]
[M ⊨ T] [Infinite M] : ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable := by
classical
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
·
exact fun t =>
isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans (aleph0_le_lift.2 (aleph0_le_mk M)))
· apply Monotone.directed_le
refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
simp only [Finset.coe_map, Function.Embedding.coe_subtype]
exact
Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s)) Set.monotone_image fun _ _ =>
Finset.coe_subset.2
